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 -- Martin Escardo http://www.cs.bham.ac.uk/~mhe