# HG changeset patch
# User wenzelm
# Date 1396869091 -7200
# Node ID 34480050397423e7d58c1dd0548f62012e8cd04b
# Parent  1e77ed11f2f78b9c7d03dd172a6568ee61a9b7de
provide old-style ISABELLE_SCALA_SCRIPT for uniformity;

diff -r 1e77ed11f2f7 -r 344800503974 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Apr 07 13:06:34 2014 +0200
+++ b/lib/scripts/getsettings	Mon Apr 07 13:11:31 2014 +0200
@@ -46,6 +46,7 @@
 #key executables
 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
+ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
 
 function isabelle ()
 {
@@ -59,7 +60,7 @@
 
 function isabelle_scala_script ()
 {
-  "$ISABELLE_HOME/bin/isabelle_scala_script" "$@"
+  "$ISABELLE_SCALA_SCRIPT" "$@"
 }
 
 #platform