[Agda] Multi-line comments in literate Agda files

[Marko Dimjašević]

On Fri, 2020-09-11 at 15:11 +0200, Nils Anders Danielsson wrote:
> 
> The following seems to work:
> 
> ```
> {-# OPTIONS --warning=noOverlappingTokensWarning #-}
> 
> {-
> ```
> 
> ```
> -}
> ```


Thank you Nils, that did the trick! I just had to put the pragma at the
very beginning of the file. Opening a multi-line comment in a code block
then comments out everything until the closing delimiter.

Uma, thank you for your suggestion! What Nils proposed requires less typing
from me, so I'll go with his proposal.


--
Kind regards,
Marko

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200911/94abf850/attachment.sig>