aboutsummaryrefslogtreecommitdiff
path: root/html-test/src/PatternSyns.hs
diff options
context:
space:
mode:
authorPhil Ruffwind <rf@rufflewind.com>2015-09-30 02:22:43 -0400
committerBen Gamari <ben@smart-cactus.org>2016-02-08 17:51:21 +0100
commit1b6bcd62e7f5534be45a0d5737b76d181c2d934b (patch)
treecff5673e3bf990748c1b75cb7d25f19d8dd6283f /html-test/src/PatternSyns.hs
parent228a0d72baa04be161b0fc918266f2edb0c6519b (diff)
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).
Diffstat (limited to 'html-test/src/PatternSyns.hs')
0 files changed, 0 insertions, 0 deletions