scripts: Allow running with any mes.
authorJan Nieuwenhuizen <janneke@gnu.org>
Sun, 26 Mar 2017 20:09:24 +0000 (22:09 +0200)
committerJan Nieuwenhuizen <janneke@gnu.org>
Sun, 26 Mar 2017 20:09:24 +0000 (22:09 +0200)
* scripts/mescc.mes: Run $MES if set, default to ../scripts/mes.
* scripts/repl.mes: Likewise.

scripts/mescc.mes
scripts/repl.mes

index 9994fda9c7e835ccaa3a6705e78245b3ae2a309c..fac99d7db06027f8f6f5453e02e2208323e5cd04 100755 (executable)
@@ -1,7 +1,8 @@
 #! /bin/sh
 # -*-scheme-*-
+MES=${MES-$(dirname $0)/mes}
 prefix=module/
-echo '()' | cat $prefix/mes/base-0.mes $0 /dev/stdin | $(dirname $0)/mes $MES_FLAGS "$@"
+echo '()' | cat $prefix/mes/base-0.mes $0 /dev/stdin | $MES $MES_FLAGS "$@"
 #paredit:||
 chmod +x a.out
 exit $?
index ac32000a8b5804d21437457f1faebe61dd692a7c..f14655885c1fda5415f22116dbc8fd96f5dccac7 100755 (executable)
@@ -1,9 +1,10 @@
 #! /bin/sh
 # -*-scheme-*-
-MES_ARENA=${MES_ARENA-20000000}
+MES=${MES-$(dirname $0)/mes}
+MES_ARENA=${MES_ARENA-30000000}
 export MES_ARENA
 prefix=module/
-cat $prefix/mes/base-0.mes $0 /dev/stdin | $(dirname $0)/mes $MES_FLAGS "$@"
+cat $prefix/mes/base-0.mes $0 /dev/stdin | $MES $MES_FLAGS "$@"
 #paredit:|
 exit $?
 !#