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).
parent
228a0d72
No related branches found
No related tags found
Showing
- haddock-api/resources/html/Ocean.std-theme/ocean.css 4 additions, 9 deletionshaddock-api/resources/html/Ocean.std-theme/ocean.css
- haddock-api/src/Haddock/Backends/Xhtml/Layout.hs 7 additions, 4 deletionshaddock-api/src/Haddock/Backends/Xhtml/Layout.hs
- haddock-api/src/Haddock/Backends/Xhtml/Names.hs 3 additions, 3 deletionshaddock-api/src/Haddock/Backends/Xhtml/Names.hs
- haddock-api/src/Haddock/Backends/Xhtml/Utils.hs 1 addition, 1 deletionhaddock-api/src/Haddock/Backends/Xhtml/Utils.hs
Loading
Please register or sign in to comment