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 +-
 library/library.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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
diff --git a/library/library.ml b/library/library.ml
index be0c259979..e4169d66e0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -314,7 +314,7 @@ let fetch_table what dp (f,pos,digest) =
     if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
     let table, pos', digest' = System.marshal_in_segment f ch in
     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') digest') then raise Faulty;
     let () = close_in ch' in
     table
-- 
cgit v1.2.3