makeString(char c)
  /**
   * make a String from a char
   */

  static String makeString(char c)
    {
    return (new StringBuffer(1).append(c)).toString();
    }