gawk exit doesn't exit promptly

[Boemker, Tim]

gawk's exit statement appears not to terminate gawk until all of the
input records have been read.
In the following example, gawk never exits, even though the exit
statement has been executed:

$ cat a
a
$ tail -f a | gawk '{ print "exiting"; exit }'
exiting