From b3382afa4dafc8d97a2c3d58398cb29936ff1416 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 28 Oct 2019 15:47:37 +0100
Subject: [PATCH] feat: add bin/lean_wrapped helper script that chooses the
 right stage and use it in lean-mode

---
 bin/lean_wrapped             | 17 +++++++++++++++++
 lean4-mode/lean4-settings.el |  2 +-
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100755 bin/lean_wrapped

diff --git a/bin/lean_wrapped b/bin/lean_wrapped
new file mode 100755
index 0000000000..514584110f
--- /dev/null
+++ b/bin/lean_wrapped
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+# Call `lean_stage0` when in library/Init; otherwise call `lean`.
+
+bin=$(dirname $(realpath $0))
+lib=$(dirname $bin)/library/Init
+# use dir of input file, or pwd if stdin
+if [[ "$*" == *--stdin* ]]; then
+    dir=$(pwd)
+else
+    dir=$(dirname $(realpath ${@:$#}))
+fi
+# check if `dir` starts with `lib`
+if [[ ${dir##$lib} != $dir ]]; then
+    $bin/lean_stage0 $*
+else
+    $bin/lean $*
+fi
diff --git a/lean4-mode/lean4-settings.el b/lean4-mode/lean4-settings.el
index 505843e80b..f174432d76 100644
--- a/lean4-mode/lean4-settings.el
+++ b/lean4-mode/lean4-settings.el
@@ -22,7 +22,7 @@
   (cl-case system-type
     ('windows-nt   "lean.exe")
     ('cygwin       "lean.exe")
-    (t             "lean"))
+    (t             "lean_wrapped"))
   "Default executable name of Lean")
 
 (defcustom lean4-rootdir nil