# HG changeset patch
# User wenzelm
# Date 1620387468 -7200
# Node ID 0da9e824255fa5d56a9789d453a6e37518a6bdd5
# Parent  f4778e08dcd75316aa8274a770f007c1ecd3a999# Parent  9b4579e5bcedba2b7d1f0620d04ce89adbe6c8fd
merged

diff -r 9b4579e5bced -r 0da9e824255f Admin/init
--- a/Admin/init	Fri May 07 13:34:01 2021 +0200
+++ b/Admin/init	Fri May 07 13:37:48 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