# HG changeset patch
# User wenzelm
# Date 950095804 -3600
# Node ID 504689622489040f037fdf6dde24310c2164132c
# Parent  6c4bec5cd2ac6023f41967ca6958b9822b1d5fbc
document -c;

diff -r 6c4bec5cd2ac -r 504689622489 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Feb 09 12:29:03 2000 +0100
+++ b/src/Pure/Thy/present.ML	Wed Feb 09 12:30:04 2000 +0100
@@ -327,7 +327,7 @@
 (* finish session *)
 
 fun isatool_document doc_format doc_prefix =
-  let val cmd = "$ISATOOL document -o '" ^ doc_format ^ "' '" ^ File.sysify_path 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;
 
 fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;