From 5a96856d68ed89cdf01d8e0264c90bd88da61de2 Mon Sep 17 00:00:00 2001
From: Kovid Goyal <kovid@kovidgoyal.net>
Date: Tue, 24 Nov 2020 13:17:27 +0530
Subject: [PATCH] Fix custom css file not being included

---
 manual/conf.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/manual/conf.py b/manual/conf.py
index 81aa89da0f..0bd6d0613d 100644
--- a/manual/conf.py
+++ b/manual/conf.py
@@ -148,6 +148,7 @@ html_favicon = '../icons/favicon.ico'
 # relative to this directory. They are copied after the built-in static files,
 # so a file named "default.css" will overwrite the built-in "default.css".
 html_static_path = ['resources', '../icons/favicon.ico']
+html_css_files = ['custom.css']
 
 # If not '', a 'Last updated on:' timestamp is inserted at every page bottom,
 # using the given strftime format.