diff -r d9f4285c795c -r 2f5dea574a75 docs/src/header.html --- a/docs/src/header.html Sat Oct 28 11:25:27 2017 +0200 +++ b/docs/src/header.html Sat Oct 28 15:43:51 2017 +0200 @@ -40,8 +40,15 @@