diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-04 20:34:01 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-04 20:34:44 +0200 |
| commit | ba5efb7b2eac8fc4c2e166d0057f6c17f81c2fd6 (patch) | |
| tree | 89585260a80bc17ce3bdd11f98a74a210cd78543 /tools/coqdoc | |
| parent | bd0e8ce51ed8eb8359d198fb5d14d14381847200 (diff) | |
Prevent verbatim text from leaking out of comments. (See bug #2882)
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index d8a30ee36..d1cb0d3d8 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 } |