function ARGS()

in src/executil.js [25:31]


function ARGS (s, var_args) {
    const ret = s.trim().split(/\s+/);
    for (let i = 1; i < arguments.length; ++i) {
        ret.push(arguments[i]);
    }
    return ret;
}