EESSI/docs

Drop "Home" tab

Closed this issue · 1 comments

Is there a way to drop the "Home" tab in the header? That introduces a lot of space that is useless unless we add more tabs (and the logo already performs the home function)

With this change:

diff --git a/mkdocs.yml b/mkdocs.yml
index 3a0740a..9c519d4 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -14,7 +14,7 @@ repo_name: EESSI @ GitHub
 repo_url: https://github.com/EESSI
 edit_uri: docs/edit/master/docs
 nav:
-  - Home: index.md
+  - "": index.md
   - Project overview: overview.md
   - Filesystem layer: filesystem_layer.md
   - Compatibility layer: compatibility_layer.md

The Home at the top and the left menu disappears (back to home then requires clicking the tiny logo top left), but it doesn't make the banner smaller. That needs less trivial customization, see https://squidfunk.github.io/mkdocs-material/customization/