From 85cae9c42e93957188a2a94c83daf7c0a639dbd7 Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Wed, 20 May 2026 10:39:31 +0100
Subject: [PATCH] chore: hide "show imports" and "show imported by" commands in
 command palette

---
 vscode-lean4/package.json | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
index 2d25355c..bb82b72f 100644
--- a/vscode-lean4/package.json
+++ b/vscode-lean4/package.json
@@ -1273,11 +1273,11 @@
                 },
                 {
                     "command": "lean4.leanModuleHierarchy.showImports",
-                    "when": "lean4.isLeanFeatureSetActive"
+                    "when": "false"
                 },
                 {
                     "command": "lean4.leanModuleHierarchy.showImportedBy",
-                    "when": "lean4.isLeanFeatureSetActive"
+                    "when": "false"
                 }
             ],
             "editor/title": [