aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a06702e0d..7d84ecf6c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -277,6 +277,7 @@ and read_vernac_file verbosely s =
close_input in_chan input; (* we must close the file first *)
match e with
| End_of_input ->
+ cur_file := None;
if do_beautify () then
pr_new_syntax (Loc.make_loc (max_int,max_int)) None
| _ -> raise_with_file fname (disable_drop e, info)