mirror of
https://gerrit.googlesource.com/git-repo
synced 2025-02-24 02:06:12 +00:00
To avoid noise due to the passage of time, don't regenerate man pages if the only thing different is the datestamp in the header. Change-Id: Ic8d7b08d12e59c66994c0cc2d4ec2d2ed3eb6e6d Reviewed-on: https://gerrit-review.googlesource.com/c/git-repo/+/318575 Reviewed-by: Jack Neus <jackneus@google.com> Reviewed-by: Mike Frysinger <vapier@google.com> Tested-by: Mike Frysinger <vapier@google.com>
These are helper tools for managing official releases. See the release process document for more details.