diff -r ae368664625f -r 8acf182f6424 docs/src/header.html --- a/docs/src/header.html Fri Jul 05 15:07:43 2019 +0200 +++ b/docs/src/header.html Fri Jul 05 15:47:57 2019 +0200 @@ -21,6 +21,7 @@