// Various utilities
Array.prototype.copy = function(){ return [].concat(this); };
Array.prototype.copyFrom = function(src){ return [].concat(src); };

String.prototype.trim = function() { return this.replace(/^\s+|\s+$/g, ""); };