From 0520fa60a855b4c5f7b9d9298607cfd9e346c0e3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 26 Apr 2020 14:25:22 +0200
Subject: Open object files in binary mode.

---
 checker/check.ml  | 2 +-
 lib/objFile.ml    | 4 ++--
 vernac/library.ml | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/checker/check.ml b/checker/check.ml
index 8554c5a677..31bfebc3d5 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -333,7 +333,7 @@ let intern_from_file ~intern_mode (dir, f) =
       let seg_opaque = ObjFile.get_segment ch ~segment:"opaques" in
       let () = ObjFile.close_in ch in
       (* Actually read the data *)
-      let ch = open_in f in
+      let ch = open_in_bin f in
 
       let (sd:summary_disk) = marshal_in_segment ~validate ~value:Values.v_libsum ~segment:seg_sd f ch in
       let (md:library_disk) = marshal_in_segment ~validate ~value:Values.v_lib ~segment:seg_md f ch in
diff --git a/lib/objFile.ml b/lib/objFile.ml
index 190b1833bd..96db51a010 100644
--- a/lib/objFile.ml
+++ b/lib/objFile.ml
@@ -143,7 +143,7 @@ let marshal_out_segment h ~segment v =
   let pos' = LargeFile.pos_out ch in
   let len = Int64.sub pos' pos in
   let hash =
-    let in_ch = open_in h.out_filename in
+    let in_ch = open_in_bin h.out_filename in
     let () = LargeFile.seek_in in_ch pos in
     let digest = Digest.channel in_ch (Int64.to_int len) in
     let () = close_in in_ch in
@@ -163,7 +163,7 @@ let marshal_out_binary h ~segment =
     let pos' = LargeFile.pos_out ch in
     let len = Int64.sub pos' pos in
     let hash =
-      let in_ch = open_in h.out_filename in
+      let in_ch = open_in_bin h.out_filename in
       let () = LargeFile.seek_in in_ch pos in
       let digest = Digest.channel in_ch (Int64.to_int len) in
       let () = close_in in_ch in
diff --git a/vernac/library.ml b/vernac/library.ml
index 8a10891dfb..35b2a18871 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -58,7 +58,7 @@ let in_delayed f ch ~segment =
 let fetch_delayed del =
   let { del_digest = digest; del_file = f; del_off = pos; } = del in
   try
-    let ch = open_in f in
+    let ch = open_in_bin f in
     let () = LargeFile.seek_in ch pos in
     let obj = System.marshal_in f ch in
     let digest' = Digest.input ch in
-- 
cgit v1.2.3