diff options
| author | Maxime Dénès | 2016-06-05 12:41:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-05 12:47:01 +0200 |
| commit | e6b0ab5079186b7dba643a04e6222a4260de96ff (patch) | |
| tree | ad403847daf29799661aa787db5934e20462cae7 /checker/check.ml | |
| parent | 835bd9f8eb19f617dcbda625450fc8ed57048e49 (diff) | |
Fix incorrect checking of library checksums.
Since d09def34, only the summary of libraries was included in the checksum, not
the actual content of the library. This quick fix performs the checking of the
checksum immediately, even if the loading is delayed.
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/check.ml b/checker/check.ml index 3a5c91217d..b6b790dcfb 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -304,7 +304,7 @@ let intern_from_file (dir, f) = try let ch = System.with_magic_number_check raw_intern_library f in let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in - let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in + let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in let (discharging:'a option), _, _ = System.marshal_in_segment f ch in let (tasks:'a option), _, _ = System.marshal_in_segment f ch in |