From 8c9c796d7ea52bcaea882df8c4e6ae57a3189979 Mon Sep 17 00:00:00 2001 From: Guillaume Gomez Date: Fri, 4 Mar 2022 14:10:10 +0100 Subject: [PATCH 1/3] Make theme selector button visible even for non-local pages --- src/librustdoc/html/static/js/main.js | 5 ----- src/librustdoc/html/templates/page.html | 2 +- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/src/librustdoc/html/static/js/main.js b/src/librustdoc/html/static/js/main.js index 8e1919f75d671..f79a1f56eb549 100644 --- a/src/librustdoc/html/static/js/main.js +++ b/src/librustdoc/html/static/js/main.js @@ -135,15 +135,10 @@ function hideThemeButtonState() { // Set up the theme picker list. (function () { - if (!document.location.href.startsWith("file:///")) { - return; - } var themeChoices = getThemesElement(); var themePicker = getThemePickerElement(); var availableThemes = getVar("themes").split(","); - removeClass(themeChoices.parentElement, "hidden"); - function switchThemeButtonState() { if (themeChoices.style.display === "block") { hideThemeButtonState(); diff --git a/src/librustdoc/html/templates/page.html b/src/librustdoc/html/templates/page.html index baadd3c27b446..8728578259364 100644 --- a/src/librustdoc/html/templates/page.html +++ b/src/librustdoc/html/templates/page.html @@ -108,7 +108,7 @@

{%- endif -%} {#- -#} {#- -#} {#- -#}
{{- content|safe -}}
{#- -#} From 4744c19318d75168722ce3742d1cf73b9a21ab5a Mon Sep 17 00:00:00 2001 From: Guillaume Gomez Date: Fri, 4 Mar 2022 15:35:30 +0100 Subject: [PATCH 3/3] Display theme picker button on mobile too --- src/librustdoc/html/static/css/rustdoc.css | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/librustdoc/html/static/css/rustdoc.css b/src/librustdoc/html/static/css/rustdoc.css index 001af73611198..0743a1d84640d 100644 --- a/src/librustdoc/html/static/css/rustdoc.css +++ b/src/librustdoc/html/static/css/rustdoc.css @@ -1835,12 +1835,6 @@ details.rustdoc-toggle[open] > summary.hideme::after { margin-left: 32px; } - /* Space is at a premium on mobile, so remove the theme-picker icon. */ - .theme-picker { - display: none; - width: 0; - } - .content { margin-left: 0px; }