aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornotin2010-01-28 15:38:11 +0000
committernotin2010-01-28 15:38:11 +0000
commit077010072dc158df72a0557b26fe8770256dad42 (patch)
tree590869cf1c97d97fe11c040478f157b5208621e2
parentb5c4711e721bfb9a168838d91d76fc20b7db16c9 (diff)
Correction du bug #2219: application du patch envoyé par F. Garillot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12695 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tools/coqdoc/cpretty.mll6
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 4f1406cc83..3b889c59ab 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -693,7 +693,7 @@ and doc_bol = parse
| eof
{ true }
| '_'
- { start_emph ();
+ { if !Cdglobals.plain_comments then start_emph () Output.char '%';
doc None lexbuf }
| _
{ backtrack lexbuf; doc None lexbuf }
@@ -840,10 +840,10 @@ and doc indents = parse
doc indents lexbuf}
| nonidentchar '_'
{ Output.char (lexeme_char lexbuf 0);
- start_emph ();
+ if !Cdglobals.plain_comments then start_emph () else Output.char '%';
doc indents lexbuf }
| '_' nonidentchar
- { stop_emph ();
+ { if !Cdglobals.plain_comments then stop_emph () else Output.char '%';
Output.char (lexeme_char lexbuf 1);
doc indents lexbuf }
| eof