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)devel
devel
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.