function trim(s) {

    var s2 = s.replace(/^\s*/, "");
    return s2.replace(/\s*$/, "");

} // function