Should nextfile in BEGINFILE skip ENDFILE?

[Ed Morton]

I see in the documentation for nextfile 
(https://www.gnu.org/software/gawk/manual/gawk.html#Nextfile-Statement) 
it says (emphasis mine):

> In |gawk|, execution of |nextfile| causes additional things to happen: 
> any |ENDFILE| rules are executed **if |gawk| is not currently in an 
> |END| or |BEGINFILE| rule**, |ARGIND| is incremented, and any 
> |BEGINFILE| rules are executed. (|ARGIND| hasn’t been introduced yet. 
> See section Predefined Variables 
> <https://www.gnu.org/software/gawk/manual/gawk.html#Built_002din-Variables>.) 
>
>
> With |gawk|, |nextfile| is useful inside a |BEGINFILE| rule to skip 
> over a file that would otherwise cause |gawk| to exit with a fatal 
> error. In this case, **|ENDFILE| rules are not executed**. 

which seems to be clearly saying that when you call `nextfile` inside a 
`BEGINFILE` block the `ENDFILE` block isn't executed and yet when I do 
that in gawk 5.1.0 on cygwin I see it is:

$ awk 'BEGINFILE{print "a"; nextfile} ENDFILE{print "b"}' /dev/null
a
b

Is that a bug or a documentation issue?

    Ed.