Stream: Coq devs & plugin devs

Topic: odoc complaints

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)

Emilio Jesús Gallego Arias (Sep 14 2021 at 10:57):

Unfortunately yes, dev doc needs more work, see issue

Emilio Jesús Gallego Arias (Sep 14 2021 at 10:58):

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

Emilio Jesús Gallego Arias (Sep 14 2021 at 10:58):

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

Last updated: Oct 12 2024 at 12:01 UTC