Community
Participate
Working Groups
See https://bugs.eclipse.org/bugs/show_bug.cgi?id=562200#c2
Philippe, can you take this one too?
New Gerrit change created: https://git.eclipse.org/r/161688
No UI changes is expected in this bug
Gerrit change https://git.eclipse.org/r/161688 was merged to [master]. Commit: http://git.eclipse.org/c/platform/eclipse.platform.ui.git/commit/?id=4203cd1b8c5e092b4109254ad1fa2fa25f3916fd
Thanks Philippe