summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-08-01 11:59:20 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-08-01 11:59:20 +0000
commita83f0c1710cc5143dd885e84c94e14f7d3216f93 (patch)
tree448bfcfa371854f5abeba9dcb6fd9944d98521cc /doc
parent4c8a550fae641115170e4fc9c1b1292834e0c6c0 (diff)
Plus besoin de rectifier les URL invalides
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@707 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc')
-rw-r--r--doc/removeproofs.mll2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll
index d4b2431..7fb37bb 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 }