diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-29 11:59:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-29 11:59:11 +0000 |
| commit | 62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd (patch) | |
| tree | e4d7d609af1b03ffa12b7c7c0ce4e08ea06303ca /interp/dumpglob.ml | |
| parent | 97da8221e0097ed365f0a99e4960148424a59734 (diff) | |
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
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 19 |
1 files changed, 17 insertions, 2 deletions
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 |