From a8f8e7116b155ba0bd7965d55fe310d10984dbc6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jul 2015 16:10:30 -0700
Subject: [PATCH] feat(bin): add auxiliary scripts that allow us to test
 lean-emacs mode in the build directory (i.e., without installing Lean)

---
 bin/leanemacs_build     | 8 ++++++++
 bin/leanemacs_build.bat | 4 ++++
 2 files changed, 12 insertions(+)
 create mode 100755 bin/leanemacs_build
 create mode 100644 bin/leanemacs_build.bat

diff --git a/bin/leanemacs_build b/bin/leanemacs_build
new file mode 100755
index 000000000..ea1fe78f1
--- /dev/null
+++ b/bin/leanemacs_build
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+MY_PATH="`dirname \"$0\"`"              # relative
+MY_PATH="`( cd \"$MY_PATH\" && pwd )`"  # absolutized and normalized
+
+export LEAN_ROOTDIR="$MY_PATH/.."
+export LEAN_EMACS_PATH="$LEAN_ROOTDIR/src/emacs"
+
+emacs -load $LEAN_EMACS_PATH/load-lean.el $*
diff --git a/bin/leanemacs_build.bat b/bin/leanemacs_build.bat
new file mode 100644
index 000000000..6000c8c2c
--- /dev/null
+++ b/bin/leanemacs_build.bat
@@ -0,0 +1,4 @@
+SET MY_PATH=%~dp0
+SET LEAN_ROOTDIR=%MY_PATH%/..
+SET LEAN_EMACS_PATH=%MY_PATH%/../src/emacs
+emacs -load %LEAN_EMACS_PATH%/load-lean.el