diff options
| author | Manish Goregaokar <manishsmail@gmail.com> | 2020-07-15 11:01:18 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-15 11:01:18 -0700 |
| commit | 0d07db98ab5870c269493cb9fba9376b9477d4b4 (patch) | |
| tree | 40635b873b0f98453a16a94245ac76f17f9dccb9 | |
| parent | efad203144c25ba6f34e8e53d4c1a7417fb03c23 (diff) | |
| parent | 2ca24b618e40e92f8061419928dcd0f1f15527e5 (diff) | |
| download | rust-0d07db98ab5870c269493cb9fba9376b9477d4b4.tar.gz rust-0d07db98ab5870c269493cb9fba9376b9477d4b4.zip | |
Rollup merge of #74218 - GuillaumeGomez:search-results-bottom-margin, r=Dylan-DPC
Add margin after doc search results I found it not really on computer that the last result is right at the bottom of the page. I find it better with margin below (especially when you hover the last element!). A screenshot to show the result:  r? @kinnison cc @rust-lang/rustdoc @Manishearth @jyn514
| -rw-r--r-- | src/librustdoc/html/static/rustdoc.css | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/librustdoc/html/static/rustdoc.css b/src/librustdoc/html/static/rustdoc.css index a3f4dc55fe7..15a0c76ceea 100644 --- a/src/librustdoc/html/static/rustdoc.css +++ b/src/librustdoc/html/static/rustdoc.css @@ -364,6 +364,7 @@ nav.sub { #results > table { width: 100%; table-layout: fixed; + margin-bottom: 40px; } .content pre.line-numbers { |