Patch: PR java/5923

[Tom Tromey]

>>>>> "Tom" == Tom Tromey <tromey@redhat.com> writes:

Tom> This patch fixes PR 5923.
Tom> Ok for trunk and branch?

Alex approved this off-list.
I'm checking it in.

Tom