From 018fe0b19e52f44b4025b0c311de631ecb53d936 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Vladim=C3=ADr=20Vondru=C5=A1?= <mosra@centrum.cz>
Date: Tue, 9 Jun 2020 14:10:26 +0200
Subject: [PATCH] documentation/python: list forgotten default option, avoid
 duplicates.

---
 documentation/python.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/documentation/python.py b/documentation/python.py
index 5daa149f..0c750426 100755
--- a/documentation/python.py
+++ b/documentation/python.py
@@ -135,12 +135,13 @@ default_config = {
     'PROJECT_SUBTITLE': None,
     'PROJECT_LOGO': None,
     'MAIN_PROJECT_URL': None,
+
     'INPUT': None,
     'OUTPUT': 'output',
     'INPUT_MODULES': [],
     'INPUT_PAGES': [],
     'INPUT_DOCS': [],
-    'OUTPUT': 'output',
+
     'THEME_COLOR': '#22272e',
     'FAVICON': 'favicon-dark.png',
     'STYLESHEETS': [
@@ -153,6 +154,7 @@ default_config = {
         ('Classes', 'classes', [])],
     'LINKS_NAVBAR2': [],
 
+    'HTML_HEADER': None,
     'PAGE_HEADER': None,
     'FINE_PRINT': '[default]',
     'FORMATTED_METADATA': ['summary'],
-- 
2.30.2