diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-31 09:25:29 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-31 09:25:29 +0200 |
| commit | bc480550dbd705384bec15968dbdde0987df311c (patch) | |
| tree | eb1cb668ea5eaff8231d223a4d27711443639d58 /tools/coqdoc | |
| parent | 41e4725805588b3fffdfdc0cd5ee6859de1612b5 (diff) | |
Do not escape "'" when outputting to html, especially not using "´".
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/output.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index ae6e6388f..06030c45a 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -595,7 +595,6 @@ module Html = struct | '<' -> Buffer.add_string buff "<" | '>' -> Buffer.add_string buff ">" | '&' -> Buffer.add_string buff "&" - | '\'' -> Buffer.add_string buff "´" | '\"' -> Buffer.add_string buff """ | c -> Buffer.add_char buff c done; |