add links to every document, fixes #5515

This commit is contained in:
narimiran
2019-02-16 17:06:09 +01:00
committed by Dominik Picheta
parent 51c43218c9
commit a0fb77dfd5

View File

@@ -77,7 +77,20 @@ $content
doc.body_toc = """
<div class="row">
<div class="three columns">
<div>
<div id="global-links">
<ul class="simple-boot">
<li>
<a href="manual.html">Manual</a>
</li>
<li>
<a href="lib.html">Standard library</a>
</li>
<li>
<a href="theindex.html">Index</a>
</li>
</ul>
</div>
<div id="searchInputDiv">
Search: <input type="text" id="searchInput"
onkeyup="search()" />
</div>