--- a/lib/Tools/usedir Tue Oct 23 19:15:00 2001 +0200
+++ b/lib/Tools/usedir Tue Oct 23 22:51:30 2001 +0200
@@ -188,7 +188,7 @@
[ "$COMPRESS" = true ] && OPT_C="-c"
"$ISABELLE" \
- -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \
+ -e "Session.use_dir true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \
$OPT_C -q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
@@ -197,7 +197,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE" \
- -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \
+ -e "Session.use_dir false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..