tex_source: Buffer.write;
authorwenzelm
Thu, 07 Oct 1999 12:20:21 +0200
changeset 7769 700439dc581e
parent 7768 b106e4af1301
child 7770 0497323c1f0b
tex_source: Buffer.write;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Oct 07 12:19:47 1999 +0200
+++ b/src/Pure/Thy/present.ML	Thu Oct 07 12:20:21 1999 +0200
@@ -329,7 +329,7 @@
     val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
 
     fun finish_node (a, {tex_source, html_source = _, html}) =
-     (apsome (fn p => Buffer.write_nonempty (Path.append p (tex_path a)) tex_source) doc_prefix;
+     (apsome (fn p => Buffer.write (Path.append p (tex_path a)) tex_source) doc_prefix;
       Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
   in
     seq finish_node (Symtab.dest theories);