diff options
| author | letouzey | 2013-08-22 14:29:29 +0000 |
|---|---|---|
| committer | letouzey | 2013-08-22 14:29:29 +0000 |
| commit | d475ff0d4427fc1c3859fc5d8d0cb7cc0a32a14e (patch) | |
| tree | a75a8640a512b580569038dcd48ec5b35c9870e2 /lib/system.ml | |
| parent | 1f3331bd4ff9fd562d534554185db2b6c4cc9e78 (diff) | |
Change in vo format : digest aren't Marshalled anymore
Since digests are strings (of size 16), we just dump them
now in vo files (cf. Digest.output) instead of using Marshal
on them : this is cleaner and saves a few bytes.
Increased VOMAGIC to clearly identify this change in the format.
Please rerun ./configure after this commit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/lib/system.ml b/lib/system.ml index d2788de93f..37b8dee4c4 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -114,12 +114,17 @@ let try_remove filename = msg_warning (str"Could not remove file " ++ str filename ++ str" which is corrupted!") -let marshal_out ch v = Marshal.to_channel ch v [] +let error_corrupted file = error (file ^ " is corrupted, try to rebuild it.") + +let marshal_out ch v = Marshal.to_channel ch v []; flush ch let marshal_in filename ch = try Marshal.from_channel ch - with - | End_of_file | Failure _ (* e.g. "truncated object" *) -> - error (filename ^ " is corrupted, try to rebuild it.") + with End_of_file | Failure _ -> error_corrupted filename + +let digest_out = Digest.output +let digest_in filename ch = + try Digest.input ch + with End_of_file | Failure _ -> error_corrupted filename exception Bad_magic_number of string |