Community
Participate
Working Groups
We should activate the save action on it to avoid such things.
New Gerrit change created: https://git.eclipse.org/r/56103
Gerrit change https://git.eclipse.org/r/56103 was merged to [master]. Commit: http://git.eclipse.org/c/platform/eclipse.platform.ui.git/commit/?id=08487dc22586cbbe8a9fb8a6a8b51e978edb0ff4
.