# HG changeset patch
# User wenzelm
# Date 954612560 -7200
# Node ID 1a2c5ccebfdb7a4d58623ca703f6f4e72dd42dc2
# Parent  40036a2ab64608c8465a209582c15d522dc39c27
isatool document: check output file (workaround PolyML problem with RC);

diff -r 40036a2ab646 -r 1a2c5ccebfdb src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Mar 31 22:39:39 2000 +0200
+++ b/src/Pure/Thy/present.ML	Sat Apr 01 20:09:20 2000 +0200
@@ -327,8 +327,14 @@
 (* finish session *)
 
 fun isatool_document doc_format doc_prefix =
-  let val cmd = "$ISATOOL document -c -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'"
-  in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end;
+  let
+    val cmd = "$ISATOOL document -c -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'";
+  in
+    writeln cmd;
+    if system cmd <> 0 orelse not (File.exists (Path.ext doc_format doc_prefix)) then
+      error "Failed to build document"
+    else ()
+  end;
 
 fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;