affeldt-aist / coq2html

An HTML documentation generator for Coq source files
GNU General Public License v2.0
1 stars 3 forks source link

fix: link name of notations #21

Closed yoshihiro503 closed 8 months ago

yoshihiro503 commented 8 months ago

fixes #8

Make link name of notations MD5 hash string if the path contains characters other than alphabets, number, or some symbols. This behavior is same as current coqdoc implementation.

spec

Paths consisting only of the following characters will not be hashed:

reference implementation of coqdoc

https://github.com/coq/coq/blob/v8.19/tools/coqdoc/output.ml#L617

issues