[Agda] how do I quote agda code on the agda wiki?

[James Wood]

I came across the same problem just the other day, but in inline code,
so this workaround isn't available (as far as I can tell). If it's
possible to turn on UTF8 support for the wiki, this would surely be helpful.

James

On 21/05/2020 19:26, Ingo Blechschmidt wrote:
> Dear Thorsten,
> 
> On Thu 21 May 2020 05:47:12 PM GMT, Thorsten Altenkirch wrote:
>> I was just adding an item to
>> https://wiki.portal.chalmers.se/agda/Main/AIMXXXII
>> and tried to add some agda code (I know an unusual thing to do a=on the agda wiki)
> [...]
> 
> I don't know enough about PmWiki, and therefore will refrain from
> updating the "Basic editing" page, but I just fixed the formatting on
> the page you linked.
> 
> To render code as code, without funny HTML entities ("ℕ" and their
> like), you may not use [@...@] but do have to indent the code.
> 
> Cheers,
> Ingo
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>