diff options
Diffstat (limited to 'haddock-api')
| -rw-r--r-- | haddock-api/resources/html/NewOcean.std-theme/new-ocean.css | 4 | 
1 files changed, 2 insertions, 2 deletions
| 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 906b3954..456052f1 100644 --- a/haddock-api/resources/html/NewOcean.std-theme/new-ocean.css +++ b/haddock-api/resources/html/NewOcean.std-theme/new-ocean.css @@ -83,7 +83,7 @@ body.js-enabled .hide-when-js-enabled {      top: 10.2em;      left: 2em;      bottom: 1em; -    overflow-y: scroll; +    overflow-y: auto;    }    #synopsis { @@ -94,7 +94,7 @@ body.js-enabled .hide-when-js-enabled {      bottom: 1em;      right: 0;      max-width: 65vw; -    overflow-y: scroll; +    overflow-y: auto;      /* Ensure that synopsis covers everything (including MathJAX markup) */      z-index: 1;    } | 
