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 /driver/Frontend.ml | |
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
Diffstat (limited to 'driver/Frontend.ml')
0 files changed, 0 insertions, 0 deletions