function echo(args: Array<string>): string {
var buf = "";
buf += args.join(' ');
buf += "\n";
return buf;
}
export { echo };