# HG changeset patch
# User wenzelm
# Date 961971797 -7200
# Node ID 20a70ef9c32043936a79760277935470e000d092
# Parent  6180c29d2db64ae87d9e558d073808274f8cd114
tuned;

diff -r 6180c29d2db6 -r 20a70ef9c320 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Jun 26 00:00:40 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Jun 26 00:23:17 2000 +0200
@@ -104,7 +104,7 @@
   \%%% Local Variables:\n\
   \%%% mode: latex\n\
   \%%% TeX-master: \"root\"\n\
-  \%%% End:\n%";
+  \%%% End:\n";
 
 fun old_symbol_source name syms =
   isabelle_file ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);