From e6b0ab5079186b7dba643a04e6222a4260de96ff Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 5 Jun 2016 12:41:16 +0200 Subject: 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. --- checker/check.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/check.ml') diff --git a/checker/check.ml b/checker/check.ml index 3a5c91217..b6b790dcf 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 -- cgit v1.2.3