Move the permalinks to "#" on the right side

Since pull request #407, the identifiers have been permalinked to
themselves, but this makes it difficult to copy the identifier by
double-clicking.  To work around this usability problem, the permalinks
are now placed on the far right adjacent to "Source", indicated by "#".

Also, 'namedAnchor' now uses 'id' instead of 'name' (which is obsolete).

1 files changed, 4 insertions, 9 deletions

diff --git a/haddock-api/resources/html/Ocean.std-theme/ocean.css b/haddock-api/resources/html/Ocean.std-theme/ocean.css
index 139335ac..fcf23810 100644
--- a/haddock-api/resources/html/Ocean.std-theme/ocean.css
+++ b/haddock-api/resources/html/Ocean.std-theme/ocean.css
@@ -381,21 +381,16 @@ div#style-menu-holder {
 #interface h5 + div.top {
  	margin-top: 1em;
 }
-#interface p.src .link {
+#interface .src .selflink,
+#interface .src .link {
   float: right;
   color: #919191;
-  border-left: 1px solid #919191;
   background: #f0f0f0;
   padding: 0 0.5em 0.2em;
-  margin: 0 -0.5em 0 0.5em;
+  margin: 0 -0.5em 0 0;
 }
-
-#interface td.src .link {
-  float: right;
-  color: #919191;
+#interface .src .selflink {
   border-left: 1px solid #919191;
-  background: #f0f0f0;
-  padding: 0 0.5em 0.2em;
   margin: 0 -0.5em 0 0.5em;
 }