# HG changeset patch # User wenzelm # Date 1666030685 -7200 # Node ID a39fa81929d439e04841521ded7a6f7b0b13d33f # Parent 14cf5a50c1e940dec36ed3afe0cfdab1d52560f7 avoid spurious error messages, e.g. when scala is missing; diff -r 14cf5a50c1e9 -r a39fa81929d4 lib/scripts/getsettings --- a/lib/scripts/getsettings Mon Oct 17 16:10:45 2022 +0200 +++ b/lib/scripts/getsettings Mon Oct 17 20:18:05 2022 +0200 @@ -130,7 +130,7 @@ fi if [ -e "$ISABELLE_SETUP_JAR" ]; then - ISABELLE_SETUP_CLASSPATH="$(isabelle_jdk java -classpath "$(platform_path "$SCALA_INTERFACES:$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath)" + ISABELLE_SETUP_CLASSPATH="$(isabelle_jdk java -classpath "$(platform_path "$SCALA_INTERFACES:$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath 2>/dev/null)" fi set +o allexport