Admin/init
changeset 73640 f4778e08dcd7
parent 73589 479e9b17090e
child 73705 ac07f6be27ea
equal deleted inserted replaced
73639:e1432539df35 73640:f4778e08dcd7
   151   echo "Changed \$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER: \"$OLD_IDENTIFIER\" ~> \"$IDENTIFIER\""
   151   echo "Changed \$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER: \"$OLD_IDENTIFIER\" ~> \"$IDENTIFIER\""
   152   echo "Changed \$ISABELLE_HOME_USER: \"$OLD_ISABELLE_HOME_USER\" ~> \"$ISABELLE_HOME_USER\""
   152   echo "Changed \$ISABELLE_HOME_USER: \"$OLD_ISABELLE_HOME_USER\" ~> \"$ISABELLE_HOME_USER\""
   153 fi
   153 fi
   154 
   154 
   155 if [ -z "$VERSION" ]; then
   155 if [ -z "$VERSION" ]; then
   156   "$ISABELLE_HOME/bin/isabelle" components -I || exit "?$"
   156   "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
   157   "$ISABELLE_HOME/bin/isabelle" components -a || exit "?$"
   157   "$ISABELLE_HOME/bin/isabelle" components -a || exit "$?"
   158   if [ -n "$BUILD_OPTIONS" ]; then
   158   if [ -n "$BUILD_OPTIONS" ]; then
   159     "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
   159     "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
   160   fi
   160   fi
   161 elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
   161 elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
   162   fail "Not a repository clone: cannot switch version"
   162   fail "Not a repository clone: cannot switch version"