devel to main While Keeping the Branch History CleanAll updates are made in the devel branch and merged to main via Pull Requests. This is done for security and consistency (as per repository Rules).
However, as updates accumulate, PRs can become cluttered or conflicted, making merges difficult. This guide describes a procedure to keep both branches in sync and avoid such issues.
⚠ Caution:
If you follow the full procedure, unmerged commits in devel may be lost. For routine work, it’s usually enough to just “6. Reset devel to match main (after PR is merged)”.
devel onto main (resolving conflicts if required)develdevel to main on GitHub Webdevel to match main git fetch origin
git checkout devel
devel onto the latest main git rebase origin/main
git add <conflicted-files>
git rebase --continue
git rebase -i origin/main
pick to squash for all but the first commit, then save and exit.devel to GitHub git push --force-with-lease origin devel
devel to main on GitHub WebIf files are identical, the diff may be empty or minimal.
This creates a single, clean commit on
main.
devel to match main (after PR is merged)devel for new work.
git checkout devel
git fetch origin
git reset --hard origin/main
git push --force-with-lease origin devel
devel after merging avoids endless loops and keeps branches synchronized.