max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: write .c output file in binary mode for reproducibility

Browse source
This commit is contained in:
Sebastian Ullrich 2021-09-15 14:41:07 +02:00
parent 23c3dc335b
commit da516f5aa7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/shell.cpp
View file

@ -644,7 +644,7 @@ extern "C" int lean_main(int argc, char ** argv) {
}
if (c_output && ok) {
std::ofstream out(*c_output);
std::ofstream out(*c_output, std::ios_base::binary);
if (out.fail()) {
std::cerr << "failed to create '" << *c_output << "'\n";
return 1;