On Sun, Jun 26, 2022 at 5:19 AM Noboru Saito <noborusai(at)gmail(dot)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