Hi, On Sun, 2003-08-10 at 01:14, Mark Wielaard wrote: > On Sat, 2003-08-02 at 17:58, Tom Tromey wrote: > > I think this patch that should go upstream, since it only touches > > eclipse.org code. Stick it in the eclipse.org bugzilla and tell me > > the bug number. I'll vote for it :-) > > This is now bug #41361 > https://bugs.eclipse.org/bugs/show_bug.cgi?id=41361 Which got almost immediately applied. Wow, those eclipse guys are fast with accepting patches. Cheers, Mark