src/Pure/Tools/fontforge.scala
changeset 71601 97ccf48c2f0c
parent 71163 b5822f4c3fde
child 75393 87ebf5a50283
--- 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(", ",", ")")
   }