From fbfd22c08fbcd418f85ea9bad4667a7e91bb95ac Mon Sep 17 00:00:00 2001
From: Sebastiaan van Stijn <github@gone.nl>
Date: Thu, 9 Jul 2020 12:28:18 +0200
Subject: [PATCH] Fix missing "toggle" for right-hand navigation

This button was accidentally removed when the archives were
removed in ba85012f47efdc41e30ad9e9f7a9a579d05f6382

Signed-off-by: Sebastiaan van Stijn <github@gone.nl>
---
 _includes/navigation.html | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/_includes/navigation.html b/_includes/navigation.html
index ca586c6c5e..4d130e076b 100644
--- a/_includes/navigation.html
+++ b/_includes/navigation.html
@@ -26,4 +26,7 @@
 
         </ul>
     </div>
+    <div class="ctrl-right">
+        <a href="javascript:void(0)" id="menu-toggle"><i class="fa fa-indent" aria-hidden="true"></i></a>
+    </div>
 </div>