# HG changeset patch
# User wenzelm
# Date 1164304195 -3600
# Node ID 2f83b11c301bdb800211c21c0d41bf5dfd10e647
# Parent  4ce7425c837292dce57d85e1fe921789971bd13f
added ISABELLE_IDENTIFIER;
removed THIS_IS_ISABELLE_BUILD magic;

diff -r 4ce7425c8372 -r 2f83b11c301b lib/scripts/getsettings
--- a/lib/scripts/getsettings	Thu Nov 23 18:49:03 2006 +0100
+++ b/lib/scripts/getsettings	Thu Nov 23 18:49:55 2006 +0100
@@ -22,6 +22,14 @@
 ISABELLE="$ISABELLE_HOME/bin/isabelle-process"
 ISATOOL="$ISABELLE_HOME/bin/isatool"
 
+#Isabelle version
+ISABELLE_VERSION=$("$ISABELLE_HOME/lib/Tools/version")
+if [ "$ISABELLE_VERSION" = "Isabelle repository version" ]; then
+  ISABELLE_IDENTIFIER=""
+else
+  ISABELLE_IDENTIFIER="$ISABELLE_VERSION"
+fi
+
 #users tend to put strange things in here ...
 unset ENV
 unset BASH_ENV
@@ -50,19 +58,13 @@
 [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
 
-#produce ML system and Isabelle version identifier
+#ML system identifier
 if [ -z "$ML_PLATFORM" ]; then
   ML_IDENTIFIER="$ML_SYSTEM"
 else
   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
 fi
 
-ISABELLE_VERSION=$("$ISABELLE_HOME/lib/Tools/version")
-if [ "$ISABELLE_VERSION" != "Isabelle repository version" -a "$THIS_IS_ISABELLE_BUILD" != true ]
-then
-  ML_IDENTIFIER="${ML_IDENTIFIER}_${ISABELLE_VERSION}"
-fi
-
 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
 
 set +o allexport