# HG changeset patch
# User wenzelm
# Date 1430655130 -7200
# Node ID 52d02564242a055c06233d5e373c01135d18f722
# Parent  d47387d4a3c6823670d05f1d998288227c942dd4
tuned message;

diff -r d47387d4a3c6 -r 52d02564242a src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat May 02 13:58:06 2015 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun May 03 14:12:10 2015 +0200
@@ -109,7 +109,7 @@
   {
     val max_user_fonts = 2
     if (Symbol.font_names.length > max_user_fonts)
-      error("Too many user symbol fonts (max " + max_user_fonts + " permitted): " +
+      error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
         Symbol.font_names.mkString(", "))
 
     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
@@ -448,4 +448,3 @@
     }
   }
 }
-