Community
Participate
Working Groups
New Gerrit change created: https://git.eclipse.org/r/59227
Gerrit change https://git.eclipse.org/r/59227 was merged to [master]. Commit: http://git.eclipse.org/c/pde/eclipse.pde.ui.git/commit/?id=5bfe980da9660879c3b79a6cdb764b5bc4147d86
.
Lars, can you please verify this one.
Verified by code inspection