# HG changeset patch
# User wenzelm
# Date 1380045464 -7200
# Node ID 86c8f15afd88324e5f2b1002c376e061310139cd
# Parent  b1bc857f2422e77d8a739047f375882d20981792
clarified font;

diff -r b1bc857f2422 -r 86c8f15afd88 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Sep 24 19:53:05 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Sep 24 19:57:44 2013 +0200
@@ -281,10 +281,8 @@
               val fm = text_field.getFontMetrics(text_field.getFont)
               val loc =
                 SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
-              val font =
-                text_field.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
 
-              val completion = new Completion_Popup(layered, loc, font, result.items)
+              val completion = new Completion_Popup(layered, loc, text_field.getFont, result.items)
               {
                 override def complete(item: Completion.Item) {
                   PIDE.completion_history.update(item)