# HG changeset patch # User wenzelm # Date 1620384183 -7200 # Node ID f4778e08dcd75316aa8274a770f007c1ecd3a999 # Parent e1432539df35e4ca4e5ec76d53b1aa0bf72f9f53 proper "$?"; diff -r e1432539df35 -r f4778e08dcd7 Admin/init --- a/Admin/init Thu May 06 23:28:30 2021 +0200 +++ b/Admin/init Fri May 07 12:43:03 2021 +0200 @@ -153,8 +153,8 @@ fi if [ -z "$VERSION" ]; then - "$ISABELLE_HOME/bin/isabelle" components -I || exit "?$" - "$ISABELLE_HOME/bin/isabelle" components -a || exit "?$" + "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?" + "$ISABELLE_HOME/bin/isabelle" components -a || exit "$?" if [ -n "$BUILD_OPTIONS" ]; then "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS fi