aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cpretty.mll
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-01-28 15:44:45 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-01-28 15:44:45 +0000
commit5e70300acbfed51607425f132c98554e075219b3 (patch)
tree18a24a5f02fbd3d5f5ac5a7d2c8d46fd075760c8 /tools/coqdoc/cpretty.mll
parent077010072dc158df72a0557b26fe8770256dad42 (diff)
Typo in previous commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12696 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r--tools/coqdoc/cpretty.mll2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 3b889c59a..c07ae2f71 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 () Output.char '%';
+ { if !Cdglobals.plain_comments then start_emph () else Output.char '%';
doc None lexbuf }
| _
{ backtrack lexbuf; doc None lexbuf }