tuned message;
authorwenzelm
Sun May 03 14:12:10 2015 +0200 (2015-05-03)
changeset 6023852d02564242a
parent 60237 d47387d4a3c6
child 60239 755e11e2e15d
tuned message;
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sat May 02 13:58:06 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun May 03 14:12:10 2015 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4    {
     1.5      val max_user_fonts = 2
     1.6      if (Symbol.font_names.length > max_user_fonts)
     1.7 -      error("Too many user symbol fonts (max " + max_user_fonts + " permitted): " +
     1.8 +      error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
     1.9          Symbol.font_names.mkString(", "))
    1.10  
    1.11      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    1.12 @@ -448,4 +448,3 @@
    1.13      }
    1.14    }
    1.15  }
    1.16 -