Exit Value from Awk

[Guy Harris]

>Does anyone know how to set the exit code from awk within an awk
>script?

Set the exit code without exiting, no.  Exit with a particular exit
code, yes:

	$ awk 'END { exit 17 }' </dev/null
	$ echo $?
	17

If this isn't documented, it should be....