proper "$?";
authorwenzelm
Fri, 07 May 2021 12:43:03 +0200
changeset 73896 f4778e08dcd7
parent 73895 e1432539df35
child 73900 0da9e824255f
proper "$?";
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