[Agda] Absolute links in html rendering of Agda files

[Andreas Abel]

That feature was useful but wasn't working flawlessly, so it is not in 
the current development versions.  (See gallais pointer.)

On 16.02.2018 14:42, Martin Escardo wrote:
> 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
>>
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/