diff -r 74c1b51c1cd9 -r 24dae6222579 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue May 06 15:24:41 1997 +0200
+++ b/lib/scripts/getsettings	Tue May 06 15:27:35 1997 +0200
@@ -23,4 +23,9 @@
 ISABELLE=$ISABELLE_HOME/bin/isabelle
 ISATOOL=$ISABELLE_HOME/bin/isatool
 
+#append ML system to paths
+ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM"
+ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done)
+ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
+
 set +o allexport