diff -r 87c22ec6a0fd -r fed2ead878ea docs/src/header.html --- a/docs/src/header.html Sat Aug 10 08:46:38 2019 +0200 +++ b/docs/src/header.html Sat Oct 05 16:58:16 2019 +0200 @@ -21,6 +21,7 @@