Stream: Coq devs & plugin devs

Topic: odoc complaints


view this post on Zulip Gaëtan Gilbert (Sep 14 2021 at 10:55):

Is the doc:ml-api:odoc job supposed to be so full of complaints? https://gitlab.com/coq/coq/-/jobs/1584911612

File "clib/cObj.mli", line 11, characters 4-40:
'6': bad heading level (0-5 allowed).
File "clib/cObj.mli", line 24, characters 4-53:
'6': bad heading level (0-5 allowed).
File "clib/cObj.mli", line 49, characters 4-39:
'6': bad heading level (0-5 allowed).
.... (many more)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2021 at 10:57):

Unfortunately yes, dev doc needs more work, see issue

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2021 at 10:58):

https://github.com/coq/coq/issues/7155

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2021 at 10:58):

https://github.com/coq/coq/issues/14641


Last updated: Oct 16 2021 at 03:02 UTC