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