From 76bc99158d580647af6a2617f0e2d60ebc367e5c Mon Sep 17 00:00:00 2001 From: Felix Lange Date: Thu, 7 Nov 2019 15:25:36 +0100 Subject: [PATCH] [DOCS] add search box (#20251) This adds a search box (powered by DuckDuckGo site search) to the navbar. --- _layouts/default.html | 14 ++++++++++++-- static/styles/custom/common.css | 4 ++++ 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/_layouts/default.html b/_layouts/default.html index adc45ac19d..76efc89c56 100644 --- a/_layouts/default.html +++ b/_layouts/default.html @@ -31,10 +31,20 @@ common-js: diff --git a/static/styles/custom/common.css b/static/styles/custom/common.css index da3bbf3cc1..a6140ab0c7 100644 --- a/static/styles/custom/common.css +++ b/static/styles/custom/common.css @@ -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; +}