gawk: RS matching empty string

[Stepan Kasal]

Hello,
  thanks to Arnold and Andreas for fixing the RS="^..." bug.

I have another bug report.  gawk seem's to mishandle the case when
RS matches empty string, observe:

$ echo a a|./gawk 'BEGIN{RS="a*"}{print $0":"RT":"}'
:a:
:a:
:a:
$ echo a a|./gawk 'BEGIN{RS="\\<|\\>"}{print $0":"RT":"}'
a a
::
$ echo -n a a|./gawk 'BEGIN{RS="\\<|\\>"}{print $0":"RT":"}'
a ::

Yes, RS=="a*" is not useful, but the later two examples could be useful.

I understand this is not important, perhaps just the manual should say that
RS should never match an empty string.
But maybe someone will come with a miraculous hint again...

Regards,
        Stepan