From fd86ca4e159c73613eadd48d0910e25572b3addf Mon Sep 17 00:00:00 2001
From: Alexandre Dulaunoy <a@foo.be>
Date: Thu, 11 Aug 2016 12:07:05 +0200
Subject: [PATCH] Tools added in the menu

---
 _includes/header.html | 1 +
 1 file changed, 1 insertion(+)

diff --git a/_includes/header.html b/_includes/header.html
index bba3c74..e7d1dcd 100755
--- a/_includes/header.html
+++ b/_includes/header.html
@@ -50,6 +50,7 @@
                                 </ul>
                             </li>
                             <li {% if current[1] == 'documentation' %}class="current"{% endif %}><a href="{{ site.baseurl }}/documentation">Documentation</a></li>
+                            <li {% if current[1] == 'tools' %}class="current"{% endif %}><a href="{{ site.baseurl }}/tools">Tools</a></li>
                             <li {% if current[1] == 'who' %}class="current"{% endif %}><a href="{{ site.baseurl }}/who">Who</a></li>
                             <li {% if current[1] == 'communities' %}class="current"{% endif %}><a href="{{ site.baseurl }}/communities">Communities</a></li>