chore: add manual backport instructions to readme #594
Conversation
README.md
Outdated
| For example, for modifications to the reference manual associated with Lean version 4.22, the branch should be named `4.22.0`: | ||
|
|
||
| ``` | ||
| git checkout -b 4.22.0 //create new branch |
There was a problem hiding this comment.
Here, we should add a step to check if the branch exists before just creating it. If there's already a maintenance branch for a given release, it should be used.
There was a problem hiding this comment.
If the branch exists, what are the next steps? Should it be updated before any changes are pushed to it?
There was a problem hiding this comment.
It won't let you push if you don't have all the changes in it. Maybe this should be phrased in Git verbs rather than commands?
|
I suggested some minor tweaks. Otherwise, LGTM |
Co-authored-by: David Thrane Christiansen <[email protected]>
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 33581dc. |
|
@ashandoak said out of band that there were some outstanding changes to be made on his end and he'll "try to get to it again this week and will come around with questions if I decide I need to make any changes." |
3 participants
Adds manual backport instructions to README.md