michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(bin): add auxiliary scripts that allow us to test lean-emacs mode in the build directory (i.e., without installing Lean)

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-20 16:10:30 -07:00
parent 8ad6312764
commit a8f8e7116b
2 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
bin/leanemacs_build Executable file
View file

@ -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 $*

4
bin/leanemacs_build.bat Normal file
View file

@ -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