From 62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 29 Oct 2011 11:59:11 +0000
Subject: Added checksums to glob files and warned about possibly missing
 packages for utf8.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/dumpglob.ml | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

(limited to 'interp/dumpglob.ml')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 26f4d4e19..4a8756b88 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -31,8 +31,6 @@ let noglob () = glob_output := NoGlob
 
 let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
 
-let multi_dump () = !glob_output = MultFiles
-
 let dump_to_dotglob f = glob_output := MultFiles
 
 let dump_into_file f = glob_output := File f; open_glob_file f
@@ -40,6 +38,23 @@ let dump_into_file f = glob_output := File f; open_glob_file f
 let dump_string s =
   if dump () then Pervasives.output_string !glob_file s
 
+let start_dump_glob vfile =
+  match !glob_output with
+  | MultFiles ->
+      open_glob_file (Filename.chop_extension vfile ^ ".glob");
+      output_string !glob_file "DIGEST ";
+      output_string !glob_file (Digest.to_hex (Digest.file vfile));
+      output_char !glob_file '\n'
+  | File f ->
+      open_glob_file f;
+      output_string !glob_file "DIGEST NO\n"
+  | NoGlob | StdOut ->
+      ()
+
+let end_dump_glob () =
+  match !glob_output with
+  | MultFiles | File _ -> close_glob_file ()
+  | NoGlob | StdOut -> ()
 
 let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
-- 
cgit v1.2.3