sS fileNameEncode_safeChars = " "; //" ()[]#";

sS fileNameEncode(S s) {
  s = dropLeadingDots(s); // don't produce file names starting with a dot!
  new StringBuilder buf;
  int n = l(s);
  for (int i = 0; i < n; i++) {
    char c = s.charAt(i);
    if (contains(fileNameEncode_safeChars, c))
      buf.append(c);
    else
      buf.append(urlencode(str(c)));
  }
  ret str(buf);
}