From 983ca34a566c4eafe7360846f97e717a4f04124b Mon Sep 17 00:00:00 2001 From: Lala Sabathil Date: Mon, 12 Aug 2024 15:10:36 +0200 Subject: [PATCH] Update conf.py --- docs/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/conf.py b/docs/conf.py index fa0f2da368..1997510129 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -326,7 +326,7 @@ def write_new(): # so a file named "default.css" will overwrite the builtin "default.css". html_static_path = ["_static"] html_css_files = ["css/custom.css"] -html_js_files = ["js/custom.js", "js/scorer.js", "language_data.js"] +html_js_files = ["js/custom.js", "js/scorer.js", "language_data.js", "searchtools.js"] # Add any extra paths that contain custom files (such as robots.txt or # .htaccess) here, relative to this directory. These files are copied