mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Rollup merge of #74218 - GuillaumeGomez:search-results-bottom-margin, r=Dylan-DPC

Browse Source 
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:

![Screenshot from 2020-07-10 16-32-23](https://user-images.githubusercontent.com/3050060/87166097-6103a580-c2cb-11ea-81a8-12772cf20f64.png)

r? @kinnison
cc @rust-lang/rustdoc @Manishearth @jyn514
This commit is contained in:
Manish Goregaokar 2020-07-15 11:01:18 -07:00 committed by GitHub
commit 0d07db98ab
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/librustdoc/html/static/rustdoc.css
View File

@ -364,6 +364,7 @@ nav.sub {
#results > table {
width: 100%;
table-layout: fixed;
margin-bottom: 40px;
}
.content pre.line-numbers {