diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-06 13:40:37 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-06 13:40:37 +0000 |
| commit | e8015d10ba87ba61d648376caada4703cfdd0de3 (patch) | |
| tree | 8864d86f5ad6a6c142dc128e6034c784c7c586a1 | |
| parent | 7d0c6c801673543b6c6a1b7e1c58e924ab04d48a (diff) | |
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
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 () |