diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 4742a2e5dd..4f1406cc83 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -184,10 +184,10 @@ let check_start_list str = let n_dashes = count_dashes str in let (n_spaces,_) = count_spaces str in - if n_dashes >= 4 then + if n_dashes >= 4 && not !Cdglobals.plain_comments then Rule else - if n_dashes = 1 then + if n_dashes = 1 && not !Cdglobals.plain_comments then List n_spaces else Neither |