equal
deleted
inserted
replaced
34 else "\\" + ch |
34 else "\\" + ch |
35 } |
35 } |
36 } |
36 } |
37 |
37 |
38 def string(s: String): String = |
38 def string(s: String): String = |
39 if (s == "") "\"\"" |
39 if (s.isEmpty) "\"\"" |
40 else UTF8.bytes(s).iterator.map(bash_chr).mkString |
40 else UTF8.bytes(s).iterator.map(bash_chr).mkString |
41 |
41 |
42 def strings(ss: Iterable[String]): String = |
42 def strings(ss: Iterable[String]): String = |
43 ss.iterator.map(Bash.string).mkString(" ") |
43 ss.iterator.map(Bash.string).mkString(" ") |
44 |
44 |