--- 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"