mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
IJPL-212619 DevKit: mark deprecated unused API for removal
API, which was marked as deprecated in 252 or earlier and has no external and internal usages, is marked for removal. GitOrigin-RevId: ad6b23186b845ca27f7c843b132205904faa2002
This commit is contained in:
committed by
intellij-monorepo-bot
parent
a1d261d740
commit
f735882397
@@ -191,6 +191,6 @@ public interface IdeaPlugin extends DomElement {
|
||||
* @deprecated the corresponding tag in plugin.xml is not supported anymore, this method is used to highlight occurrences of such a tag
|
||||
*/
|
||||
@SuppressWarnings("SpellCheckingInspection")
|
||||
@Deprecated
|
||||
@Deprecated(forRemoval = true)
|
||||
@NotNull List<? extends Helpset> getHelpsets();
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user