diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/fontforge.scala --- a/src/Pure/Tools/fontforge.scala Fri Mar 27 13:04:15 2020 +0100 +++ b/src/Pure/Tools/fontforge.scala Fri Mar 27 22:01:27 2020 +0100 @@ -38,7 +38,7 @@ } if (s.nonEmpty && s(0) == '\\') err('\\') - s.iterator.map(escape(_)).mkString(q.toString, "", q.toString) + s.iterator.map(escape).mkString(q.toString, "", q.toString) } def file_name(path: Path): Script = string(File.standard_path(path)) @@ -121,7 +121,7 @@ } def set: Script = - List(fontname, familyname, fullname, weight, copyright, fontversion).map(string(_)). + List(fontname, familyname, fullname, weight, copyright, fontversion).map(string). mkString("SetFontNames(", ",", ")") }