Does gawk manual mention how an empty regex should be handled?

[Arkadiusz Drabczyk]

TIL that empty regex matches any string:

$ awk 'BEGIN { print "abc" ~ "" }'
1
$ awk 'BEGIN { print "abc" ~ // }'
1

It can also be reproduced with mawk, Busybox awk and FreeBSD
awk. However, I wasn't able to find an explanation of that behavior in
the gawk manual. Is it actually documented somewhere?

-- 
Arkadiusz Drabczyk <arkadiusz@drabczyk.org>