[Agda] Absolute links in html rendering of Agda files

[Martin Escardo]

Thanks, this seems to be exactly what I want, although I haven't managed 
to make it work (with Agda version 2.6.0-5135fd5). I will ask questions 
in that issue page, rather than here. Martin

On 16/02/18 12:40, guillaume.allais at ens-lyon.org wrote:
> 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
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe