# HG changeset patch
# User wenzelm
# Date 883318314 -3600
# Node ID ab441d89a2cb774b1a9476b456718ff191e7de3f
# Parent  34a53d0c8e8dbe08c64f541de614b2f110b5d297
stderr to $LOG;

diff -r 34a53d0c8e8d -r ab441d89a2cb lib/Tools/usedir
--- 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=$?
diff -r 34a53d0c8e8d -r ab441d89a2cb src/Pure/mk
--- a/src/Pure/mk	Sun Dec 28 15:05:10 1997 +0100
+++ b/src/Pure/mk	Sun Dec 28 15:11:54 1997 +0100
@@ -86,7 +86,7 @@
   $ISABELLE \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
-    -q -w RAW_ML_SYSTEM Pure > $LOG
+    -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1
 else
   ITEM="RAW"
   echo -n "Building $ITEM ... "
@@ -95,7 +95,7 @@
   $ISABELLE \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "use\"$COMPAT\";" \
-    -q -w RAW_ML_SYSTEM RAW > $LOG
+    -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1
 fi
 
 RC=$?