From 664a86e08bba7f4415fb0fdaef04c4508af702d1 Mon Sep 17 00:00:00 2001 From: Parth Shastri <31370288+cppio@users.noreply.github.com> Date: Thu, 27 Oct 2022 17:40:53 -0400 Subject: [PATCH] fix: minor style improvements --- DocGen4/Output/Template.lean | 6 +++--- static/style.css | 6 ++++++ 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index ae7878b..432d070 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -48,8 +48,8 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d

{title}

-- TODO: Replace this form with our own search
- - + +
@@ -57,7 +57,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d [site] diff --git a/static/style.css b/static/style.css index fdd5e99..2944e99 100644 --- a/static/style.css +++ b/static/style.css @@ -262,6 +262,12 @@ nav { width: 100%; } +.navframe .nav { + position: absolute; + left: 0; + margin-left: 0; +} + .internal_nav .imports { margin-bottom: 1rem; }