# HG changeset patch
# User wenzelm
# Date 1275292003 -7200
# Node ID 382a56c9f2958f48678bf76e6485a7fb411b2afb
# Parent  8517a650cfdc2dda993e2f0c8d9c5e3ee0720027
tuned;

diff -r 8517a650cfdc -r 382a56c9f295 src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Sun May 30 23:42:03 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Mon May 31 09:46:43 2010 +0200
@@ -107,7 +107,7 @@
 
   private def template(font_family: String, font_size: Int): String =
     template_head +
-    "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px }" +
+    "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
     template_tail