diff options
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f80aedbf3c..1f7b947e93 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -213,7 +213,7 @@ let rec vernac_com checknav (loc,com) = end; begin try - read_vernac_file verbosely f; + Flags.silently (read_vernac_file verbosely) f; restore_translator_coqdoc st; with reraise -> let reraise = Errors.push reraise in |