Community
Participate
Working Groups
+++ This bug was initially created as a clone of Bug #515391 +++
New Gerrit change created: https://git.eclipse.org/r/95392
Gerrit change https://git.eclipse.org/r/95392 was merged to [master]. Commit: http://git.eclipse.org/c/platform/eclipse.platform.ui.git/commit/?id=0dfd918774cf1cabbac89d7fc1b6a3765e5a7ec8
Thanks Fabian.