[Agda] id number in html?

[Jason Hu]

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
comment.

> Wouldn’t that be a bit fragile?

Yes.

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

Yes, the other scheme that I mentioned.

--
/NAD

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