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

chore: hide "show imports" and "show imported by" commands in command…

85cae9c
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning

The logs for this run have expired and are no longer available.