Session.use_dir: check parent;
authorwenzelm
Fri, 05 Feb 1999 21:11:41 +0100
changeset 6249 8bb90076cc7c
parent 6248 c31c07509637
child 6250 354848db4052
Session.use_dir: check parent;
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)