diff -r b321a3be0a38 -r c743721d566f docs/src/header.html --- a/docs/src/header.html Thu Aug 03 14:32:36 2017 +0200 +++ b/docs/src/header.html Thu Aug 03 18:29:00 2017 +0200 @@ -32,7 +32,21 @@