Merge branch 'main' of github.com:leanprover/doc-gen4 into only-linkify-lean

main
Alex J. Best 2022-11-06 21:27:31 +01:00
commit 6137c9b300
2 changed files with 9 additions and 3 deletions

View File

@ -48,8 +48,8 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
<p class="header_filename break_within">{title}</p>
-- TODO: Replace this form with our own search
<form action="https://google.com/search" method="get" id="search_form">
<input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs"/>
<input type="text" name="q" autocomplete="off"/>
<input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
<input type="text" name="q" autocomplete="off"/>&#32;
<button>Google site search</button>
</form>
</header>
@ -57,7 +57,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
[site]
<nav class="nav">
<iframe src={s!"{←getRoot}/navbar.html"} class="navframe" frameBorder="0"></iframe>
<iframe src={s!"{←getRoot}navbar.html"} class="navframe" frameBorder="0"></iframe>
</nav>
</body>
</html>

View File

@ -262,6 +262,12 @@ nav {
width: 100%;
}
.navframe .nav {
position: absolute;
left: 0;
margin-left: 0;
}
.internal_nav .imports {
margin-bottom: 1rem;
}