diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html
index 26ca901fcd22..1b41342b0de8 100644
--- a/util/gh-pages/index_template.html
+++ b/util/gh-pages/index_template.html
@@ -17,7 +17,7 @@
{# #}
{# #}
-
+ {# #}
{# #}
{# #}
{# #}
@@ -28,23 +28,6 @@
{# #}
{# #}
{# #}
- {# #}
- {# #}
- {# #}
-
{# #}
{# #}
{# #}
diff --git a/util/gh-pages/style.css b/util/gh-pages/style.css
index 4f1935ba972f..497d4b125d1b 100644
--- a/util/gh-pages/style.css
+++ b/util/gh-pages/style.css
@@ -530,7 +530,6 @@ summary {
}
}
-html:not(.js) #settings-dropdown,
html:not(.js) #menu-filters {
display: none;
}
diff --git a/util/gh-pages/theme.js b/util/gh-pages/theme.js
index a5dfeed9e8c8..5067b5a0da02 100644
--- a/util/gh-pages/theme.js
+++ b/util/gh-pages/theme.js
@@ -47,6 +47,31 @@ function setTheme(theme, store) {
}
(function() {
+ function generateSettingsButton() {
+ const dropdown = document.createElement("div");
+ dropdown.id = "settings-dropdown";
+ dropdown.classList.add("dropdown");
+ dropdown.innerHTML = `
+
+ `;
+ document.body.insertBefore(dropdown, document.body.firstChild);
+ }
+
+ generateSettingsButton();
+
// This file is loaded first. If so, we add the `js` class on the ``
// element.
document.documentElement.classList.add("js");