Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

No comment syntax in mld files #998

Open
lpw25 opened this issue Sep 13, 2023 · 2 comments
Open

No comment syntax in mld files #998

lpw25 opened this issue Sep 13, 2023 · 2 comments

Comments

@lpw25
Copy link
Contributor

lpw25 commented Sep 13, 2023

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.

@sanette
Copy link

sanette commented Dec 16, 2023

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

@panglesd
Copy link
Collaborator

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants