ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;
authorwenzelm
Thu, 23 Nov 2006 18:49:03 +0100
changeset 21489 4ce7425c8372
parent 21488 e1b260d204a0
child 21490 2f83b11c301b
ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;
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