max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(bin): add script for testing leanemacs without installing Lean

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-31 17:35:20 -08:00
parent 03f43ca629
commit 70d62245a6
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
bin/test_leanemacs Executable file
View file

@ -0,0 +1,9 @@
#!/usr/bin/env bash
# Script for testing load-lean.el without installing Lean
MY_PATH="`dirname \"$0\"`" # relative
MY_PATH="`( cd \"$MY_PATH\" && pwd )`" # absolutized and normalized
export LEAN_ROOTDIR="$MY_PATH/.."
export LEAN_EMACS_PATH="$MY_PATH/../src/emacs"
emacs -load $LEAN_EMACS_PATH/load-lean.el -debug-init