From 1fe296cd7de29c37a735c4bef4979310c25bffb3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 5 Feb 2015 17:55:10 +0100 Subject: Windows: open .vo files in binary mode --- checker/check.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 9a750858d7..3e22c4b18c 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -321,7 +321,7 @@ let intern_from_file (dir, f) = System.marshal_in_segment f ch in (* Verification of the final checksum *) let () = close_in ch in - let ch = open_in f in + let ch = open_in_bin f in if not (String.equal (Digest.channel ch pos) checksum) then errorlabstrm "intern_from_file" (str "Checksum mismatch"); let () = close_in ch in -- cgit v1.2.3