From 1b6bcd62e7f5534be45a0d5737b76d181c2d934b Mon Sep 17 00:00:00 2001 From: Phil Ruffwind Date: Wed, 30 Sep 2015 02:22:43 -0400 Subject: 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). --- haddock-api/resources/html/Ocean.std-theme/ocean.css | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) (limited to 'haddock-api/resources/html') 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; } -- cgit v1.2.3