# HG changeset patch
# User wenzelm
# Date 967487603 -7200
# Node ID 5f21379beb87a43bcc25cefdc8b031d097ceaf4e
# Parent  067c25edd1bd3f4883310205aca0b59f539fa768
tex_index: Latex.tex_trailer;

diff -r 067c25edd1bd -r 5f21379beb87 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Aug 28 20:32:55 2000 +0200
+++ b/src/Pure/Thy/present.ML	Mon Aug 28 20:33:23 2000 +0200
@@ -337,7 +337,7 @@
   in
     seq finish_node (Symtab.dest theories);
     Buffer.write (Path.append html_prefix pre_index_path) html_index;
-    doc_prefixes |> apsome (write_texes tex_index doc_indexN);
+    doc_prefixes |> apsome (write_texes (Buffer.add Latex.tex_trailer tex_index) doc_indexN);
     doc_prefixes |> apsome (isatool_document doc_format o #1);
     write_graph graph (Path.append html_prefix (graph_path "session"));
     create_index html_prefix;