isatool document: stderr to stdout;
authorwenzelm
Fri, 04 Jan 2002 19:28:57 +0100
changeset 12632 3d3e356778b5
parent 12631 7648ac4a6b95
child 12633 ad9277743664
isatool document: stderr to stdout;
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"