From 49d942bb6ea9a9a63f51d94e952c9e247f9aa682 Mon Sep 17 00:00:00 2001
From: Andreas Kloeckner <inform@tiker.net>
Date: Tue, 1 Dec 2020 18:40:46 -0600
Subject: [PATCH] Delete commented doc theme options

---
 doc/conf.py | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/doc/conf.py b/doc/conf.py
index 1972886..b501a31 100644
--- a/doc/conf.py
+++ b/doc/conf.py
@@ -93,10 +93,6 @@ todo_include_todos = False
 html_theme = "furo"
 
 html_theme_options = {
-        #"extra_nav_links": {
-        #    "🚀 Github": "https://github.com/inducer/pytools",
-        #    "💾 Download Releases": "https://pypi.python.org/pypi/pytools",
-        #    }
         }
 
 # Theme options are theme-specific and customize the look and feel of a theme
-- 
GitLab