Branch Management

[vidalt]

The latest updates to the repository had been done over the dev branch but stashed+merged on the main branch. This had led to a different commit history on both branches, which is problematic for a long-lived branch such as dev. To correct this situation, I have made a copy of dev into dev-old to preserve access to un-stashed older commits, and resetted dev to the main branch head.

Therefore, before editing the code, make sure you have checked out the current state of the dev branch. Contact me if you encounter any issues. In the future, I will only register clean (aggregated commits) on the dev branch and directly merge them (without stash) into the main, so we will not encounter again this issue.

Kind Regards,
--Thibaut

[vidalt]

Closing this issue now