From fd070d4cddd37a3674b827829991117239490b97 Mon Sep 17 00:00:00 2001 From: jonmeow Date: Wed, 7 Aug 2024 15:21:23 -0700 Subject: [PATCH] impl-comment --- website/prebuild.py | 1 + 1 file changed, 1 insertion(+) diff --git a/website/prebuild.py b/website/prebuild.py index 0ca9d8f2002dd..b8b7e6231bbae 100755 --- a/website/prebuild.py +++ b/website/prebuild.py @@ -167,6 +167,7 @@ def next(nav_order: list[int]) -> int: label_subdir("docs/guides", next(nav_order)) label_subdir("docs/project", next(nav_order), grandchild_dirs=True) label_subdir("docs/spec", next(nav_order)) + # Provide a small file to cluster implementation-related directories. label_root_file( "implementation.md", "Implementation",