Admin/init
changeset 73640 f4778e08dcd7
parent 73589 479e9b17090e
child 73705 ac07f6be27ea
--- 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