function trim(s) {
		var s1 = s.replace(/^\s+/g,"");		// remove leading spaces
		var s2 = s1.replace(/\s+$/g, "");	// remove trailing spaces

		return s2;
	}