mark TacletOptionsAction as deprecated

KeYProject · Aug 18, 2024 · 8f4ee86 · 8f4ee86
1 parent 4b68234
commit 8f4ee86
Showing 1 changed file with 1 addition and 0 deletions.
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
@@ -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 {
 
     /**