Skip to content

chore: hide "show imports" and "show imported by" commands in command palette#781

Merged
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-xywqqzouoksr
May 29, 2026
Merged

chore: hide "show imports" and "show imported by" commands in command palette#781
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-xywqqzouoksr

Conversation

@mhuisi
Copy link
Copy Markdown
Collaborator

@mhuisi mhuisi commented May 20, 2026

The correct commands are the "Show Module Hierarchy" and "Show Inverse Module Hierarchy" commands - the two commands in the title are internal implementation details of the module hierarchy UI.

@mhuisi mhuisi merged commit 17d1d08 into leanprover:master May 29, 2026
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant