# HG changeset patch
# User wenzelm
# Date 1164304143 -3600
# Node ID 4ce7425c837292dce57d85e1fe921789971bd13f
# Parent  e1b260d204a0c3bb2d937cbbb7c7eefe83ffc081
ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;

diff -r e1b260d204a0 -r 4ce7425c8372 etc/settings
--- a/etc/settings	Thu Nov 23 17:52:48 2006 +0100
+++ b/etc/settings	Thu Nov 23 18:49:03 2006 +0100
@@ -106,7 +106,7 @@
 ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
 
 # Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
 
 # Heap output location. ML system identifier is appended automatically later on.
 if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
@@ -114,7 +114,7 @@
   ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
   ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
 else
-  ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+  ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
   ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 fi