diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-28 17:14:21 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-28 17:14:21 +0000 |
| commit | 9c4e7796bc2634c4aeb1f046129b4c558115ca76 (patch) | |
| tree | 9d6627d18e564850b9182862051b2d35b687256d /tools | |
| parent | 2a384d9b4ea4b6de87d2d5a2a7259425589643cb (diff) | |
Fix previous commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12698 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -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 c07ae2f71..64cd5ff55 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -693,7 +693,7 @@ and doc_bol = parse | eof { true } | '_' - { if !Cdglobals.plain_comments then start_emph () else Output.char '%'; + { if !Cdglobals.plain_comments then Output.char '_' else start_emph (); 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); - if !Cdglobals.plain_comments then start_emph () else Output.char '%'; + if !Cdglobals.plain_comments then Output.char '_' else start_emph () ; doc indents lexbuf } | '_' nonidentchar - { if !Cdglobals.plain_comments then stop_emph () else Output.char '%'; + { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ; Output.char (lexeme_char lexbuf 1); doc indents lexbuf } | eof |