# HG changeset patch
# User wenzelm
# Date 1262638187 -3600
# Node ID 14f6df4f473d78384cc9d4f46967b7922f42a6fc
# Parent  5930c6391126c5ee6a9efcc0789113f84ac4c444
shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;

diff -r 5930c6391126 -r 14f6df4f473d lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Jan 04 20:25:56 2010 +0100
+++ b/lib/scripts/getsettings	Mon Jan 04 21:49:47 2010 +0100
@@ -25,6 +25,16 @@
 ISABELLE="$ISABELLE_PROCESS"
 ISATOOL="$ISABELLE_TOOL"
 
+function isabelle-process ()
+{
+  "$ISABELLE_PROCESS" "$@"
+}
+
+function isabelle ()
+{
+  "$ISABELLE_TOOL" "$@"
+}
+
 #Isabelle distribution identifier -- filled in automatically!
 ISABELLE_IDENTIFIER=""