diff options
Diffstat (limited to 'haddock-api/resources/html/Ocean.std-theme')
| -rw-r--r-- | haddock-api/resources/html/Ocean.std-theme/ocean.css | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/haddock-api/resources/html/Ocean.std-theme/ocean.css b/haddock-api/resources/html/Ocean.std-theme/ocean.css index 29af691b..8d3f91a9 100644 --- a/haddock-api/resources/html/Ocean.std-theme/ocean.css +++ b/haddock-api/resources/html/Ocean.std-theme/ocean.css @@ -327,10 +327,6 @@ div#style-menu-holder { } #synopsis { - display: none; -} - -.no-frame #synopsis { display: block; position: fixed; right: 0; @@ -398,6 +394,7 @@ div#style-menu-holder { background: #f0f0f0; padding: 0 0.5em 0.2em; margin: 0 -0.5em 0 0; + -moz-user-select: none; } #interface .src .selflink { border-left: 1px solid #919191; @@ -614,4 +611,8 @@ div#style-menu-holder { float: right; } +:target { + background-color: #ffff00; +} + /* @end */ |