src/Pure/Thy/present.ML
changeset 7853 a4acf1b4d5a8
parent 7802 fba7a36e8556
child 8088 6ae943d080de
     1.1 --- a/src/Pure/Thy/present.ML	Wed Oct 13 19:41:18 1999 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Wed Oct 13 19:41:35 1999 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4  
     1.5  fun isatool_document doc_format doc_prefix =
     1.6    let val cmd = "$ISATOOL document -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'"
     1.7 -  in writeln cmd; writeln (execute cmd) end;
     1.8 +  in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end;
     1.9  
    1.10  fun finish () = with_session ()
    1.11      (fn {name, html_prefix, doc_format, doc_prefix, graph_path, all_graph_path, path, ...} =>