From a69311708493efe8524aed0e9d19365f79f2fab3 Mon Sep 17 00:00:00 2001
From: Alec Theriault <alec.theriault@gmail.com>
Date: Wed, 24 Oct 2018 17:31:09 -0700
Subject: Resurrect the style-switcher

This fixes #810. Looks like things were broken during the quickjump
refactor of the JS.

For the (git) record: I do not think the style switcher is a good idea.
I'm fixing it for the same reason @mzero added it; as an answer to

  "rumblings from some that they didn't want their pixels changed on bit"
---
 haddock-api/resources/html/NewOcean.std-theme/new-ocean.css | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'haddock-api/resources/html/NewOcean.std-theme')

diff --git a/haddock-api/resources/html/NewOcean.std-theme/new-ocean.css b/haddock-api/resources/html/NewOcean.std-theme/new-ocean.css
index ca1d2aaf..e390f225 100644
--- a/haddock-api/resources/html/NewOcean.std-theme/new-ocean.css
+++ b/haddock-api/resources/html/NewOcean.std-theme/new-ocean.css
@@ -138,6 +138,7 @@ body.js-enabled .hide-when-js-enabled {
       white-space: nowrap;
       height: 40px;
       padding: 4px 1.5em 0px 1.5em;
+      overflow: visible;
 
       display: flex;
       justify-content: space-between;
@@ -336,7 +337,7 @@ ul.links li {
   padding: 0;
 }
 
-ul.links li + li:before {
+ul.links > li + li:before {
   content: '\00B7';
 }
 
@@ -428,7 +429,6 @@ pre + pre {
   font-size: 1.2em;
   text-align: left;
   margin: 0 auto;
-  overflow: hidden;
 }
 
 #package-header .caption {
@@ -480,16 +480,17 @@ div#style-menu-holder {
 }
 
 #style-menu li {
-	display: list-item;
+	display: inline-block;
 	border-style: none;
 	margin: 0;
 	padding: 0;
 	color: #000;
 	list-style-type: none;
+	border-top: 1px solid #919191
 }
 
 #style-menu li + li {
-	border-top: 1px solid #919191;
+	border-left: 1px solid #919191;
 }
 
 #style-menu a {
-- 
cgit v1.2.3