From ba5efb7b2eac8fc4c2e166d0057f6c17f81c2fd6 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 4 Apr 2014 20:34:01 +0200
Subject: Prevent verbatim text from leaking out of comments. (See bug #2882)

---
 tools/coqdoc/cpretty.mll | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tools')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index d8a30ee360..d1cb0d3d8f 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -914,6 +914,7 @@ and verbatim inline = parse
   | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | ">>" { Output.stop_verbatim inline }
+  | "*)" { Output.stop_verbatim inline; backtrack lexbuf }
   | eof { Output.stop_verbatim inline }
   | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
 
-- 
cgit v1.2.3