equal
deleted
inserted
replaced
37 |
37 |
38 def string(s: String): String = |
38 def string(s: String): String = |
39 if (s == "") "\"\"" |
39 if (s == "") "\"\"" |
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: List[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 |
45 |
45 |
46 /* process and result */ |
46 /* process and result */ |
47 |
47 |