From a83f0c1710cc5143dd885e84c94e14f7d3216f93 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 1 Aug 2008 11:59:20 +0000
Subject: [PATCH] Plus besoin de rectifier les URL invalides

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@707 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 doc/removeproofs.mll | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll
index d4b24312f..7fb37bb0b 100644
--- a/doc/removeproofs.mll
+++ b/doc/removeproofs.mll
@@ -3,12 +3,14 @@ rule process inproof oc = parse
       { process true oc lexbuf }
   | "<span class=\"keyword\">" ("Qed" | "Defined") "</span>" ' '* '.'
       { process false oc lexbuf }
+(*
   | "<a class=\"idref\" href=\"" 
     [^ '"'] + '#' '"' [^ '\n' '>']* '"' '"' '>'
     ([^ '<' '\n']+ as ident)
     "</a>"
       { if not inproof then output_string oc ident;
         process inproof oc lexbuf }
+*)
   | _
       { if not inproof then output_char oc (Lexing.lexeme_char lexbuf 0);
         process inproof oc lexbuf }
-- 
GitLab