[Agda] Absolute links in html rendering of Agda files

[Guillaume Allais]

Hi Martin,

This discussion seems relevant: https://github.com/agda/agda/issues/2604
This feature was shipped as part of 2.5.3

Cheers,
--
gallais

On 16/02/18 11:32, Martin Escardo wrote:
> Say I have a function `blah` in some Agda file. The html link of
> `blah` changes every time I change my agda file and regenerate the
> html file. Is there a way to get an absolute link that won't change,
> so that I can use it from another html document?
> Thanks,
> Martin


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/dc0179fb/attachment.sig>