# HG changeset patch # User wenzelm # Date 939291621 -7200 # Node ID 700439dc581ef758364e97ae9344cbd31f47a71d # Parent b106e4af13014dbf19c33cb3ea38109ca9371de8 tex_source: Buffer.write; diff -r b106e4af1301 -r 700439dc581e 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);