diff options
| author | Eric Huss <eric@huss.org> | 2024-03-18 08:56:12 -0700 |
|---|---|---|
| committer | Mark Rousskov <mark.simulacrum@gmail.com> | 2024-03-26 19:32:27 -0400 |
| commit | dcb198695fa9be6fda82198d4f53676a5f84edf5 (patch) | |
| tree | 9476119cde02bc7df6cb323df69fed590614f141 | |
| parent | af4c9c135a674db5c7faaebbc4f5f66a0abb8f3b (diff) | |
Fix heading anchors in doc pages.
| -rw-r--r-- | src/doc/rust.css | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/doc/rust.css b/src/doc/rust.css index e0bf64c33bc..a93c1be7d7a 100644 --- a/src/doc/rust.css +++ b/src/doc/rust.css @@ -136,6 +136,28 @@ h1 a:link, h1 a:visited, h2 a:link, h2 a:visited, h3 a:link, h3 a:visited, h4 a:link, h4 a:visited, h5 a:link, h5 a:visited {color: black;} +h1, h2, h3, h4, h5 { + /* This is needed to be able to position the doc-anchor. Ideally there + would be a <div> around the whole document, but we don't have that. */ + position: relative; +} + +a.doc-anchor { + color: black; + display: none; + position: absolute; + left: -20px; + /* We add this padding so that when the cursor moves from the heading's text to the anchor, + the anchor doesn't disappear. */ + padding-right: 5px; + /* And this padding is used to make the anchor larger and easier to click on. */ + padding-left: 3px; +} +*:hover > .doc-anchor { + display: block; +} + + /* Code */ pre, code { |