Straypenguins-Tips-Inventory

Merge devel to main While Keeping the Branch History Clean

All 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)”.


Quick Summary

  1. Update local repository
  2. Rebase devel onto main (resolving conflicts if required)
  3. Squash commits (optional but recommended)
  4. Force-push devel
  5. Open & squash-merge PR from devel to main on GitHub Web
  6. Reset devel to match main

1. Update your local repository

   git fetch origin
   git checkout devel

2. Rebase devel onto the latest main

   git rebase origin/main

3. (Optional) Squash your commits for a clean history

   git rebase -i origin/main

4. Force-push devel to GitHub

   git push --force-with-lease origin devel

5. Open & merge a Pull Request from devel to main on GitHub Web

6. Reset devel to match main (after PR is merged)


Notes