From e8015d10ba87ba61d648376caada4703cfdd0de3 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Mon, 6 May 2013 13:40:37 +0000 Subject: Close the .glob file after having saved .vo This is a no op for standard Coq, but is important for Paral-ITP, since saving the library to disk forces all frozen computations, and some of them may spit out glob data, so the file descriptor must be valid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16475 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/vernac.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel/vernac.ml') diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index beb9cd9cc..84acc9bfa 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -429,5 +429,5 @@ let compile verbosely f = if not (List.is_empty pfs) then (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1); if !Flags.xml_export then !xml_end_library (); - Dumpglob.end_dump_glob (); - Library.save_library_to ldir (long_f_dot_v ^ "o") + Library.save_library_to ldir (long_f_dot_v ^ "o"); + Dumpglob.end_dump_glob () -- cgit v1.2.3