IMPORTANT: please do not squash the commits when merging!
Futurev5 to include the formatting changes from
master and make it ready to be merged to master at any point later in the nearest future. The strategy towards including these changes is as follows:
Futurev5diverged significantly from
masterand the new formatting generates too many changes to manually resolve them. Therefore, I merged (in a regular way) to
Futuerv5all commits from
masterup to the commits that deal with formatting. The corresponding merge commit is d516e050.
- For all the formatting commits, I applied
git merge origin/master -s ours --no-ff --no-commit, which told git not to look at the changes coming from master, because we want to apply the formatting by hand, but at the same time we want to keep both histories in sync.
- I the applied
git cherry-pick -n f7b137e4that adds the pre-commit checks and adapted the CI configuration to match the one used in Gauss-on-Gaussino.
- I ran
pre-commit run --all-filesthat applied the formatting.
git commitand the corresponding commit is 88261686