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