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 /library/summary.mli | |
| 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
Diffstat (limited to 'library/summary.mli')
0 files changed, 0 insertions, 0 deletions