diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-11-05 15:16:59 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-11-05 15:19:31 +0100 |
| commit | ccfeebf91784ab34f3aacaf495c59667b9ec98b6 (patch) | |
| tree | eeac104996b382432223c5aeba3332e4ef0d2671 | |
| parent | 3d6c498c1c11ad1b73efe4a0163d17cd8e9b5e86 (diff) | |
| download | compcert-ccfeebf91784ab34f3aacaf495c59667b9ec98b6.tar.gz compcert-ccfeebf91784ab34f3aacaf495c59667b9ec98b6.zip | |
Use open_in_bin instead of open_in.
On platforms that do distinguish between text mode and binary mode,
seek_in cannot reliably be used on files opened in text mode (open_in).
The input file must therefore be opened in binary mode (open_in_bin).
Bug 34075
| -rw-r--r-- | lib/Printlines.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Printlines.ml b/lib/Printlines.ml index 135672cc..b60fdf4a 100644 --- a/lib/Printlines.ml +++ b/lib/Printlines.ml @@ -25,7 +25,7 @@ type filebuf = { the first character of line number [b.lineno]. *) let openfile f = - { chan = open_in f; + { chan = open_in_bin f; lineno = 1 } let close b = |