odoc
odoc copied to clipboard
No comment syntax in mld files
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.
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
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.