# HG changeset patch
# User wenzelm
# Date 1618681062 -7200
# Node ID a96de8bbe8a30fd383769dffc81b26e200107c12
# Parent  d1767bcb79ec835777300b16e971e54b68f5691c
more options: update ISABELLE_IDENTIFIER;

diff -r d1767bcb79ec -r a96de8bbe8a3 Admin/init
--- a/Admin/init	Fri Apr 16 23:35:20 2021 +0200
+++ b/Admin/init	Sat Apr 17 19:37:42 2021 +0200
@@ -21,6 +21,7 @@
   echo
   echo "  Options are:"
   echo "    -C           force clean working directory (no backup!)"
+  echo "    -I NAME      set \$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER (or reset via -I:)"
   echo "    -L           local history only: no pull from repository server"
   echo "    -R           version is current official release"
   echo "    -U URL       Isabelle repository server"
@@ -52,6 +53,8 @@
 #options
 
 BUILD_OPTIONS="-b"
+UPDATE_IDENTIFIER=""
+IDENTIFIER=""
 PULL="true"
 
 CLEAN_FORCE=""
@@ -62,12 +65,20 @@
 VERSION_PATH=""
 VERSION_REV=""
 
-while getopts "CLRU:V:cfnr:t" OPT
+while getopts "CI:LRU:V:cfnr:t" OPT
 do
   case "$OPT" in
     C)
       CLEAN_FORCE="--clean"
       ;;
+    I)
+      UPDATE_IDENTIFIER="true"
+      if [ "$OPTARG" = ":" ]; then
+        IDENTIFIER=""
+      else
+        IDENTIFIER="$OPTARG"
+      fi
+      ;;
     L)
       PULL=""
       ;;
@@ -123,6 +134,24 @@
 
 ## main
 
+if [ -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER" ]; then
+  OLD_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")"
+else
+  OLD_IDENTIFIER=""
+fi
+
+if [ -n "$UPDATE_IDENTIFIER" -a "$IDENTIFIER" != "$OLD_IDENTIFIER" ]; then
+  OLD_ISABELLE_HOME_USER="$("$ISABELLE_HOME/bin/isabelle" getenv -b ISABELLE_HOME_USER)"
+  if [ -n "$IDENTIFIER" ]; then
+    echo -n "$IDENTIFIER" > "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER"
+  else
+    rm -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER"
+  fi
+  ISABELLE_HOME_USER="$("$ISABELLE_HOME/bin/isabelle" getenv -b ISABELLE_HOME_USER)"
+  echo "Changed \$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER: \"$OLD_IDENTIFIER\" ~> \"$IDENTIFIER\""
+  echo "Changed \$ISABELLE_HOME_USER: \"$OLD_ISABELLE_HOME_USER\" ~> \"$ISABELLE_HOME_USER\""
+fi
+
 if [ -z "$VERSION" ]; then
   "$ISABELLE_HOME/bin/isabelle" components -I || exit "?$"
   "$ISABELLE_HOME/bin/isabelle" components -a || exit "?$"