Disable github ribbon

thelegy · Dec 13, 2023 · 6e8d86f · 6e8d86f
1 parent b4cb51d
commit 6e8d86f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/docs/docs.nix b/docs/docs.nix
@@ -162,7 +162,7 @@ with lib; let
     highlight_language = 'nix'
     project = '${repo}';
     html_theme_options = {
-      'github_banner': 'true',
+      'github_banner': 'false',
       'github_button': 'true',
       'github_user': '${owner}',
       'github_repo': '${repo}',