Skip to content

fix CoqdocJS handling of apostrophes embedded in identifiers

Björn Brandenburg requested to merge wip-CoqdocJS-apostrophe into master

CoqdocJS has special logic for dealing with identifiers ending in "'": it applies its prettifying replacement logic to the prefix before the "'" and then tacks on the "'" at the end again. However, the exception fails to correctly deal with identifiers containing a "'" in the middle of the name: in this case, everything after the "'" is simply truncated.

This patch changes the regex used to identify "'" only match if "'" is truly the last character in the identifier.

Merge request reports