You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There should either be documentation of a way to escape characters in a comment, or a way added if there isn't one already. A simple use case is the desire to use the "=" character in the comment, for example to write "let x = M in N", which seems quite common.
The text was updated successfully, but these errors were encountered:
That parser... I've made some mistakes in my life.
Can you give me the code that doesn't escape correctly? It's probably just a bug, everything except for -} should be allowed in {- normal multi-line comments -}.
Here is a testcase: https://gist.github.com/2353646
The first bit will render fine, the second bit will complain about an unmatched '=' sign (when viewed in a browser and displayed through olliserver)
(I know you're busy, this is more of an FYI than a ZOMG PLZ FIX. Take your time.)
There should either be documentation of a way to escape characters in a comment, or a way added if there isn't one already. A simple use case is the desire to use the "=" character in the comment, for example to write "let x = M in N", which seems quite common.
The text was updated successfully, but these errors were encountered: