On 07/10/2013 11:50 AM, Mickael Istria wrote:
Having said, that, we can probably change this. Please file a bug
against JDT Core.
Thanks, I'll do that.
Created bug https://bugs.eclipse.org/bugs/show_bug.cgi?id=412664 and
proposed patch with Gerrit.
--
Mickael Istria
Eclipse developer at JBoss, by Red Hat <http://www.jboss.org/tools>
My blog <http://mickaelistria.wordpress.com> - My Tweets
<http://twitter.com/mickaelistria>
_______________________________________________
platform-dev mailing list
[email protected]
https://dev.eclipse.org/mailman/listinfo/platform-dev