Stream: Coq devs & plugin devs

Topic: Is this changelog entry OK?


view this post on Zulip Michael Soegtrop (May 27 2021 at 07:49):

I just found that there is a strange changelog entry (I missed it during review and merged it):

https://github.com/coq/coq/tree/master/doc/changelog/10-standard-library/14087-q-lemmas

Is this OK or should this be brought to the same format as the others?

view this post on Zulip Gaëtan Gilbert (May 27 2021 at 08:51):

you can't see it in https://coq.github.io/doc/master/refman/changes.html so it's bad

view this post on Zulip Théo Zimmermann (May 27 2021 at 09:44):

Indeed, this should be fixed.

view this post on Zulip Michael Soegtrop (May 27 2021 at 17:53):

OK, I will do a PR.


Last updated: Oct 16 2021 at 02:03 UTC