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 b1c3d2b9a..beb9cd9cc 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -324,7 +324,7 @@ let rec vernac_com interpfun checknav (loc,com) = in let psh = default_set_timeout () in try - rollback interpfun Cerrors.process_vernac_interp_error v + rollback interpfun Cerrors.process_vernac_interp_error v; restore_timeout psh; with reraise -> let reraise = Errors.push reraise in |