From da516f5aa72c8271deb1af20c83cb176a42d0edc Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 15 Sep 2021 14:41:07 +0200
Subject: [PATCH] fix: write .c output file in binary mode for reproducibility

---
 src/util/shell.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/shell.cpp b/src/util/shell.cpp
index 31aa39e03c..e557d9238d 100644
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -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;