Closed iloveeclipse closed 1 month ago
See https://github.com/eclipse-jdt/eclipse.jdt.ui/issues/1465
Before: options there but disabled
After: options gone
See https://github.com/eclipse-jdt/eclipse.jdt.ui/issues/1465