From 0e5934b9ff0fe009263a5de961fc1d9186d889f8 Mon Sep 17 00:00:00 2001 From: Takeshi KOMIYA Date: Sun, 21 Jan 2018 21:02:07 +0900 Subject: [PATCH] Fix #4472: DOCUMENTATION_OPTIONS is not defined --- CHANGES | 1 + sphinx/themes/basic/{ => static}/documentation_options.js_t | 0 2 files changed, 1 insertion(+) rename sphinx/themes/basic/{ => static}/documentation_options.js_t (100%) diff --git a/CHANGES b/CHANGES index ab9e4e10e..22a5f5936 100644 --- a/CHANGES +++ b/CHANGES @@ -23,6 +23,7 @@ Bugs fixed * #4415: autodoc classifies inherited classmethods as regular methods * #4415: autodoc classifies inherited staticmethods as regular methods +* #4472: DOCUMENTATION_OPTIONS is not defined Testing -------- diff --git a/sphinx/themes/basic/documentation_options.js_t b/sphinx/themes/basic/static/documentation_options.js_t similarity index 100% rename from sphinx/themes/basic/documentation_options.js_t rename to sphinx/themes/basic/static/documentation_options.js_t