src/Pure/System/bash.scala

--- a/src/Pure/System/bash.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/System/bash.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -35,10 +35,10 @@
 
   def string(s: String): String =
     if (s == "") "\"\""
-    else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
+    else UTF8.bytes(s).iterator.map(bash_chr).mkString
 
   def strings(ss: List[String]): String =
-    ss.iterator.map(Bash.string(_)).mkString(" ")
+    ss.iterator.map(Bash.string).mkString(" ")
 
 
   /* process and result */