diff options
| author | Enrico Tassi | 2015-12-11 16:13:56 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-12-11 16:13:56 +0100 |
| commit | f943e8d62fe88b0e387f94f23e1990b996d9f8a3 (patch) | |
| tree | 6624edeaf39fe46432b8c6e198a8a103bb71569e /etc/utils | |
| parent | 006565bdb5b473afff5f834e4b20320bb0a419fd (diff) | |
8.5 coqdoc does not want _ to be escaped + more .css classes
Diffstat (limited to 'etc/utils')
| -rw-r--r-- | etc/utils/builddoc_lib.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/etc/utils/builddoc_lib.sh b/etc/utils/builddoc_lib.sh index 0ab4fbd..4a8731f 100644 --- a/etc/utils/builddoc_lib.sh +++ b/etc/utils/builddoc_lib.sh @@ -43,7 +43,9 @@ sed -r -e ' /\(\*\*/,/\*\*\)/s/\$/$$/g; /\(\*\*/,/\*\*\)/s/\[/#[#/g; /\(\*\*/,/\*\*\)/s/]/#]#/g; - /\(\*\*/,/\*\*\)/s/\_/#\_#/g; + + # only in 8.4 + # /\(\*\*/,/\*\*\)/s/\_/#\_#/g; # the lexer glues sharp with other symbols /\(\*\*/,/\*\*\)/s/([^A-Za-z0-9 ])#\[#/\1 #[#/g; |