From 28350f46d85dc9bd14774541e0ff8cfbe210f2f8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 1 May 2020 18:08:07 +0200
Subject: [PATCH] feat: prevent Windows error message boxes in all Lean
 programs

---
 src/Init/Lean/Compiler/IR/EmitC.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Compiler/IR/EmitC.lean b/src/Init/Lean/Compiler/IR/EmitC.lean
index f0219f9120..b85837c669 100644
--- a/src/Init/Lean/Compiler/IR/EmitC.lean
+++ b/src/Init/Lean/Compiler/IR/EmitC.lean
@@ -147,7 +147,16 @@ match d with
      emitLn "void lean_initialize();"
   else
      emitLn "void lean_initialize_runtime_module();";
-  emitLn "int main(int argc, char ** argv) {\nlean_object* in; lean_object* res;";
+  emitLn "
+#if defined(WIN32) || defined(_WIN32)
+#include <windows.h>
+#endif
+
+int main(int argc, char ** argv) {
+#if defined(WIN32) || defined(_WIN32)
+SetErrorMode(SEM_FAILCRITICALERRORS);
+#endif
+lean_object* in; lean_object* res;";
   if usesLeanAPI then
     emitLn "lean_initialize();"
   else