From a226588a5e00b34b3b081b22b7da886b4f39d8d0 Mon Sep 17 00:00:00 2001
From: Jan Nieuwenhuizen <janneke@gnu.org>
Date: Sun, 26 Mar 2017 22:09:24 +0200
Subject: [PATCH] scripts: Allow running with any mes.

* scripts/mescc.mes: Run $MES if set, default to ../scripts/mes.
* scripts/repl.mes: Likewise.
---
 scripts/mescc.mes | 3 ++-
 scripts/repl.mes  | 5 +++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/scripts/mescc.mes b/scripts/mescc.mes
index 9994fda9..fac99d7d 100755
--- a/scripts/mescc.mes
+++ b/scripts/mescc.mes
@@ -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 $?
diff --git a/scripts/repl.mes b/scripts/repl.mes
index ac32000a..f1465588 100755
--- a/scripts/repl.mes
+++ b/scripts/repl.mes
@@ -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 $?
 !#
-- 
2.31.1