# HG changeset patch
# User wenzelm
# Date 1010168937 -3600
# Node ID 3d3e356778b53f0f8a4f8314efdecb79fc03e1e3
# Parent  7648ac4a6b9506386b0152d5124dff643d4d29f6
isatool document: stderr to stdout;

diff -r 7648ac4a6b95 -r 3d3e356778b5 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Jan 04 19:24:43 2002 +0100
+++ b/src/Pure/Thy/present.ML	Fri Jan 04 19:28:57 2002 +0100
@@ -313,7 +313,9 @@
 fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;
 
 fun isatool_document doc_format path =
-  let val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^ File.quote_sysify_path path in
+  let val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^
+    File.quote_sysify_path path ^ " 2>&1"
+  in
     writeln s;
     if system s <> 0 orelse not (File.exists (Path.ext doc_format path)) then
       error "Failed to build document"