diff -r ae16f162f973 -r a17f46352df3 lib/Tools/makeall --- a/lib/Tools/makeall Thu Feb 06 18:31:27 1997 +0100 +++ b/lib/Tools/makeall Thu Feb 06 18:33:50 1997 +0100 @@ -21,9 +21,6 @@ # -noexec don't execute, just check settings and IsaMakefiles -. $ISABELLE_HOME/lib/scripts/getplatform -export ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM" - set -e #fail immediately upon errors # process command line switches