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 /vernac | |
| parent | e16aab42641f0b79827c4598bf065b1607a08c43 (diff) | |
Open object files in binary mode.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/library.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |