public interface SettingsListener
Modifier and Type | Method and Description |
---|---|
void |
settingsChanged(java.util.EventObject e)
called by the Settings object to inform the listener that its
state has changed
|
Copyright © 2003-2019 The KeY-Project.