From 03a31bd0de9f6200be2eb4e49672d0ae1083c747 Mon Sep 17 00:00:00 2001 From: Jon Ross-Perkins Date: Thu, 10 Apr 2025 15:55:38 -0700 Subject: [PATCH] Drop explorer from website (#5291) Noticed this while preparing #5290, I think it can be split out. --- website/prebuild.py | 1 - 1 file changed, 1 deletion(-) diff --git a/website/prebuild.py b/website/prebuild.py index a2d56657aba2..80fca1e7ab07 100755 --- a/website/prebuild.py +++ b/website/prebuild.py @@ -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")