Improve instructions about using git notes

Notable record the commands that can be used to recover from a conflict
with the server version of the notes (merging notes is more involved and
usually not worth it, they can just be re-added after resetting).
This commit is contained in:
Vadim Zeitlin 2021-01-16 16:08:32 +01:00
parent 1065e61ab7
commit bc4f78598d

View File

@ -182,9 +182,28 @@ NOTE: This file is updated only before the release, please use
$ git log --notes=changelog --format='%N' v3.1.4..|grep .
to see all the change log entries since the last release and use
to see all the change log entries since the last release.
$ git notes --ref=changelog add -m 'wxPort: description.' to update it.
To update the notes, fetch them first:
$ git fetch origin refs/notes/changelog:refs/notes/changelog
then use the following command to update them locally
$ git notes --ref=changelog add -m 'wxPort: description.'
and finally push it to the server.
$ git push origin refs/notes/changelog:refs/notes/changelog
If this fails due to a conflict because you had forgotten to
run git-fetch first, you can always reset your local notes
(LOSING YOUR CHANGES TO THEM, so make sure to make a copy)
$ git fetch origin refs/notes/changelog
$ git update-ref refs/notes/changelog FETCH_HEAD
and then redo "git-notes add" and git-push.
3.1.4: (released 2020-07-22)