odoc icon indicating copy to clipboard operation
odoc copied to clipboard

No comment syntax in mld files

Open lpw25 opened this issue 2 years ago • 3 comments

I think there is currently no syntax for comments in odoc's syntax. This is fine within documentation comments, but less fine in .mld files.

lpw25 avatar Sep 13 '23 12:09 lpw25

Indeed, I have auto-generated mld files, so I would like to start these files with a line # auto-generated file but I don't know how to do this

sanette avatar Dec 16 '23 08:12 sanette

As a work-around, you can use comments in html-specific backend:

{%html: <!-- auto-generated file --> %}

or as @lpw25 suggested in another channel, you can abuse the backend specific syntax, which allows for non-existing backends:

{%comment: auto-generated file %}

The first one will be included in a generated html as a comment, the second one won't.

panglesd avatar Dec 18 '23 08:12 panglesd