# HG changeset patch
# User wenzelm
# Date 1164221604 -3600
# Node ID c7892915ed10582dd393c4d6d89d3fc023a0ebf6
# Parent  4b0d5e8796cc37326508eda3d9b053761bc65091
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;

diff -r 4b0d5e8796cc -r c7892915ed10 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Nov 22 17:38:36 2006 +0100
+++ b/lib/scripts/getsettings	Wed Nov 22 19:53:24 2006 +0100
@@ -50,12 +50,19 @@
 [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; }
 
-#append ML system identifier to paths
+#produce ML system and Isabelle version 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