static S removeAtName(S s) {
  if (s.startsWith("<@")) {
    int i = s.indexOf('>');
    if (i >= 0)
      ret s.substring(i+1).trim();
  }
  ret s;
}