diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java index faabacc3b5f..215114b6d7e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java @@ -13,6 +13,7 @@ // This class is not used anymore as taclet options should be set through the general settings // dialog +@Deprecated public class TacletOptionsAction extends MainWindowAction { /**