search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

Line numbers are useless without file names #30

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

I'm not sure what to make of

Line 383, character 58, warning: missing newline after ">>" block
Line 19, character 3, warning: unterminated inline ">>"
Line 135, character 6, warning: missing newline after ">>" block
Line 146, character 79, warning: missing newline after ">>" block
Line 115, character 8, warning: missing newline after ">>" block
Line 83, character 65, warning: missing newline after ">>" block
Line 26, character 6, warning: unterminated inline ">>"
Line 32, character 6, warning: unterminated inline ">>"
Line 7, character 6, warning: unterminated inline ">>"
Line 59, character 6, warning: unterminated inline ">>"
Line 347, character 6, warning: unterminated inline ">>"
Line 354, character 6, warning: unterminated inline ">>"
Line 360, character 9, warning: unterminated inline ">>"
Line 14, character 8, warning: unterminated inline ">>"
Line 26, character 8, warning: unterminated inline ">>"
Line 63, character 8, warning: unterminated inline ">>"
Line 87, character 6, warning: unterminated inline ">>"
Line 109, character 6, warning: unterminated inline ">>"
Line 125, character 6, warning: unterminated inline ">>"
Line 17, character 6, warning: unterminated inline ">>"
Line 23, character 6, warning: unterminated inline ">>"
Line 25, character 6, warning: unterminated inline ">>"
Line 151, character 6, warning: unterminated inline ">>"
Line 176, character 6, warning: unterminated inline ">>"
Line 308, character 6, warning: unterminated inline ">>"
Line 128, character 8, warning: unterminated inline ">>"
Line 17, character 6, warning: unterminated inline ">>"
Line 23, character 6, warning: unterminated inline ">>"
Line 93, character 6, warning: unterminated inline ">>"
Line 51, character 6, warning: unterminated inline ">>"
Line 129, character 6, warning: unterminated inline ">>"
Line 279, character 6, warning: unterminated inline ">>"
Line 320, character 6, warning: unterminated inline ">>"
Line 115, character 6, warning: unterminated inline ">>"
Line 127, character 6, warning: unterminated inline ">>"
Line 97, character 24, warning: missing newline after ">>" block
Line 121, character 60, warning: missing newline after ">>" block
Line 197, character 46, warning: missing newline after ">>" block
Line 154, character 14, warning: missing newline after ">>" block
Line 272, character 14, warning: missing newline after ">>" block
Line 367, character 14, warning: missing newline after ">>" block
Line 731, character 9, warning: unterminated inline ">>"
Line 737, character 9, warning: unterminated inline ">>"

at https://github.com/HoTT/HoTT/runs/2353786837?check_suite_focus=true#step:5:2860

JasonGross commented 3 years ago

Oh, sorry, this seems to be a coqdoc bug