Skip to content

Generated Agda standard library HTML has no version information #2086

Closed
@MatthewDaggitt

Description

@MatthewDaggitt

@jwaldmann writes

NB - I found it (mildly) confusing that there is no version information (in the url) at
https://agda.github.io/agda-stdlib/Data.Product.Relation.Binary.Lex.Strict.html

I wonder how we can add version information to the generated HTML? Ideally we don't really want the URL to change every time we make a release as that would make linking a nightmare....

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions