On Sun, Jun 26, 2022 at 5:19 AM Noboru Saito <noboru...@gmail.com> wrote: > The release notes have the git commit information in the comments, > it would be great to have it in the html comments as well. > > That can be done with the attached patch.
Sounds like a good idea to me. -- Peter Geoghegan
