diff options
| author | notin | 2010-01-28 15:38:11 +0000 |
|---|---|---|
| committer | notin | 2010-01-28 15:38:11 +0000 |
| commit | 077010072dc158df72a0557b26fe8770256dad42 (patch) | |
| tree | 590869cf1c97d97fe11c040478f157b5208621e2 | |
| parent | b5c4711e721bfb9a168838d91d76fc20b7db16c9 (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.mll | 6 |
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 |
