// dummy for gawk