# HG changeset patch # User wenzelm # Date 1378989122 -7200 # Node ID ffc926553ec5580455ee6bb5f6e16f381d81f2ed # Parent 602dc7e63757c614ba16f8e48207aa6180ec5960 reverse orientation of ISABELLE_CLASSPATH; diff -r 602dc7e63757 -r ffc926553ec5 lib/scripts/getsettings --- a/lib/scripts/getsettings Thu Sep 12 14:10:45 2013 +0200 +++ b/lib/scripts/getsettings Thu Sep 12 14:32:02 2013 +0200 @@ -134,7 +134,7 @@ if [ -z "$ISABELLE_CLASSPATH" ]; then ISABELLE_CLASSPATH="$X" else - ISABELLE_CLASSPATH="$X:$ISABELLE_CLASSPATH" + ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" fi done export ISABELLE_CLASSPATH