diff options
| author | Pierre-Marie Pédrot | 2020-04-26 14:25:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-26 14:59:35 +0200 |
| commit | 0520fa60a855b4c5f7b9d9298607cfd9e346c0e3 (patch) | |
| tree | c336819dc0d6253a29f450e28f95d09f5e43a24b | |
| parent | e16aab42641f0b79827c4598bf065b1607a08c43 (diff) | |
Open object files in binary mode.
| -rw-r--r-- | checker/check.ml | 2 | ||||
| -rw-r--r-- | lib/objFile.ml | 4 | ||||
| -rw-r--r-- | 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 |