# produce on stdout a file, that corresponds to the stdin file, but the
# numeric field of the VERSION field is incremented, and the REVISION
# field is reset to 0

($1 == "REVISION")	{ printf "REVISION\t0\n"; next }

($1 == "VERSION")	{ printf "VERSION\t\t%d\n", $2+1; next }

			{ print }