From d88e45c081d4dc7d4902fe5ee2ace6b320087245 Mon Sep 17 00:00:00 2001
From: Johannes Sauer <sauer@ient.rwth-aachen.de>
Date: Thu, 1 Dec 2016 15:06:25 +0100
Subject: [PATCH] we like this filename better

---
 docs/{toolboxDoku.html => toolbox.html} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename docs/{toolboxDoku.html => toolbox.html} (100%)

diff --git a/docs/toolboxDoku.html b/docs/toolbox.html
similarity index 100%
rename from docs/toolboxDoku.html
rename to docs/toolbox.html
-- 
GitLab