--- a/lib/Tools/usedir Sun Dec 28 15:05:10 1997 +0100
+++ b/lib/Tools/usedir Sun Dec 28 15:11:54 1997 +0100
@@ -113,7 +113,7 @@
$ISABELLE \
-e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
- -q -w $LOGIC $NAME >$LOG
+ -q -w $LOGIC $NAME > $LOG 2>&1
else
ITEM=$(basename $LOGIC)-"$SESSION"
echo -n "Running $ITEM ... "
@@ -121,7 +121,7 @@
$ISABELLE \
-e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
- -r -q $LOGIC > $LOG
+ -r -q $LOGIC > $LOG 2>&1
fi
RC=$?