author | wenzelm |
Fri, 07 May 2021 12:43:03 +0200 | |
changeset 73640 | f4778e08dcd7 |
parent 73639 | e1432539df35 |
child 73644 | 0da9e824255f |
Admin/init | file | annotate | diff | comparison | revisions |
--- 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