[Agda] id number in html?

Jason Hu fdhzs2010 at hotmail.com
Thu Jun 9 02:23:00 CEST 2022

Another question on html: is there a hook to add custom js file without resorting to external tools?

From: Nils Anders Danielsson<mailto:nad at cse.gu.se>
Sent: Wednesday, June 8, 2022 2:46 PM
To: Jason Hu<mailto:fdhzs2010 at hotmail.com>; agda<mailto:agda at lists.chalmers.se>
Subject: Re: [Agda] id number in html?

On 2022-06-08 15:34, Jason Hu wrote:
> If I read your answer correctly, even comments will shift the id
> number?

Yes. Note that even comments get identifiers, so you can link to a

> Wouldn’t that be a bit fragile?


> At this point, is there a way to use a different id scheme?

Yes, the other scheme that I mentioned.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220609/cd83c0de/attachment.html>

More information about the Agda mailing list