diff options
author | alexbiehl <alex.biehl@gmail.com> | 2017-08-21 20:05:42 +0200 |
---|---|---|
committer | alexbiehl <alex.biehl@gmail.com> | 2017-08-21 20:05:42 +0200 |
commit | 7a71af839bd71992a36d97650004c73bf11fa436 (patch) | |
tree | e64afbc9df5c97fde6ac6433e42f28df8a4acf49 /haddock-api/resources/html/Classic.theme | |
parent | c8a01b83be52e45d3890db173ffe7b09ccd4f351 (diff) | |
parent | 740458ac4d2acf197f2ef8dc94a66f9b160b9c3c (diff) |
Merge remote-tracking branch 'origin/master' into ghc-head
Diffstat (limited to 'haddock-api/resources/html/Classic.theme')
-rw-r--r-- | haddock-api/resources/html/Classic.theme/xhaddock.css | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/haddock-api/resources/html/Classic.theme/xhaddock.css b/haddock-api/resources/html/Classic.theme/xhaddock.css index 19dc28ec..1bf668e9 100644 --- a/haddock-api/resources/html/Classic.theme/xhaddock.css +++ b/haddock-api/resources/html/Classic.theme/xhaddock.css @@ -285,6 +285,7 @@ div.top h5 { padding: 0 8px 2px 5px; margin-right: -3px; background-color: #f0f0f0; + -moz-user-select: none; } div.subs { |