diff options
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 89bc31d0ac..d92f02ddd6 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -229,7 +229,9 @@ let rec vernac_com verbose checknav (loc,com) = if do_beautify () then pr_new_syntax loc (Some com); if !Flags.time then display_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in - interp com + let a = Lexer.com_state () in + interp com; + Lexer.restore_com_state a with reraise -> let (reraise, info) = Errors.push reraise in Format.set_formatter_out_channel stdout; |