# HG changeset patch
# User wenzelm
# Date 918245501 -3600
# Node ID 8bb90076cc7c48b322e089e2c27228d69df59de7
# Parent  c31c0750963734de4e28731cd18b3c9453e38085
Session.use_dir: check parent;

diff -r c31c07509637 -r 8bb90076cc7c lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Feb 05 21:10:19 1999 +0100
+++ b/lib/Tools/usedir	Fri Feb 05 21:11:41 1999 +0100
@@ -111,14 +111,17 @@
 
 SECONDS=0
 
+PARENT=$(basename "$LOGIC")
+
 if [ -n "$BUILD" ]; then
   ITEM="$SESSION"
   echo -n "Building $ITEM ... "
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
-    -e "Session.use_dir $RESET $INFO \"$SESSION\";" \
+    -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\";" \
     -q -w $LOGIC $NAME > $LOG 2>&1
+  RC=$?
 else
   ITEM=$(basename $LOGIC)-"$SESSION"
   echo -n "Running $ITEM ... "
@@ -126,13 +129,12 @@
 
   cd "$NAME"
   $ISABELLE \
-    -e "Session.use_dir $RESET $INFO \"$SESSION\"; quit();" \
+    -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\"; quit();" \
     -r -q $LOGIC > $LOG 2>&1
+  RC=$?
   cd ..
 fi
 
-RC=$?
-
 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)