I just found that there is a strange changelog entry (I missed it during review and merged it):
Is this OK or should this be brought to the same format as the others?
you can't see it in https://coq.github.io/doc/master/refman/changes.html so it's bad
Indeed, this should be fixed.
OK, I will do a PR.
Last updated: Oct 16 2021 at 02:03 UTC