From bc480550dbd705384bec15968dbdde0987df311c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 31 Mar 2015 09:25:29 +0200
Subject: Do not escape "'" when outputting to html, especially not using
 "&acute;".

---
 tools/coqdoc/output.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tools/coqdoc/output.ml')

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 "&lt;"
 	| '>' -> Buffer.add_string buff "&gt;"
 	| '&' -> Buffer.add_string buff "&amp;"
-        | '\'' -> Buffer.add_string buff "&acute;"
         | '\"' -> Buffer.add_string buff "&quot;"
 	| c -> Buffer.add_char buff c
       done;
-- 
cgit v1.2.3