Drop explorer from website (#5291)

Noticed this while preparing #5290, I think it can be split out.
This commit is contained in:
Jon Ross-Perkins
2025-04-10 22:55:38 +00:00
committed by GitHub
parent a94136d477
commit 03a31bd0de
-1
View File
@@ -201,7 +201,6 @@ def main() -> None:
label_subdir(
"toolchain/docs", next(nav_order), parent_title="Implementation"
)
label_subdir("explorer", next(nav_order), parent_title="Implementation")
label_subdir("testing", next(nav_order), parent_title="Implementation")