--- 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 @@
}
}
}
-