// Utils
function trim(s) {
 return s.replace(/^[ \n\t]+/, "").replace(/[ \n\t]+$/,"");
}

function log() {
  if (typeof(console)!="undefined") console.log.apply(console, arguments);
}