| changeset 37202 | 382a56c9f295 |
| parent 37164 | 8b4617ad1593 |
| child 38235 | 25d6f789618b |
--- 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