From 2bdad21e991cc6fe720635e561eb2ae9728d1986 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 12 Mar 2010 12:56:19 +0000
Subject: TeX and HTML escapes

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

(limited to 'doc/coq2html.mll')

diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index da2e602..dd7d3a9 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -372,6 +372,10 @@ and doc = parse
       { character '\n'; doc_bol lexbuf }
   | "["
       { start_bracket(); bracket lexbuf; end_bracket(); doc lexbuf }
+  | "$" [^ '\n' '$']* "$"
+      { doc lexbuf }
+  | "#" ([^ '\n' '#']* as html) "#"
+      { output_string !oc html; doc lexbuf }
   | eof
       { () }
   | _ as c
-- 
cgit v1.2.3