Closed affeldt-aist closed 8 months ago
"are th three stars before md mandatory? why not just two? (coqdoc syntax is (** IIRC so not sure a third star is needed)"
"in case we wouldn't use block comments, with stars all around, but just start ( and closing ) syntax, the less stars the better I'd say."
@proux01
fixed by PR #19
affeldt-aist
commented
8 months ago affeldt-aist
commented
8 months ago
"are th three stars before md mandatory? why not just two? (coqdoc syntax is (** IIRC so not sure a third star is needed)"
"in case we wouldn't use block comments, with stars all around, but just start ( and closing ) syntax, the less stars the better I'd say."
@proux01