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 */