[DOCS] add search box (#20251)

This adds a search box (powered by DuckDuckGo site search) to the
navbar.
This commit is contained in:
Felix Lange
2019-11-07 15:25:36 +01:00
committed by GitHub
parent 9a755be67b
commit 76bc99158d
2 changed files with 16 additions and 2 deletions

View File

@ -50,3 +50,7 @@ table thead tr th, table tbody tr td {
border-bottom: 1px solid #ddd;
padding: 4px;
}
.navbar-input-group-fixup {
margin-top: 5px;
}