diff -r 6e3c4036a80c -r e8146a561e73 docs/src/header.html --- a/docs/src/header.html Wed May 02 18:47:22 2018 +0200 +++ b/docs/src/header.html Wed May 02 19:16:58 2018 +0200 @@ -21,17 +21,17 @@