diff -r 3fc7f813b53d -r d78619cc5a4d docs/src/header.html --- a/docs/src/header.html Sun Dec 15 18:43:01 2019 +0100 +++ b/docs/src/header.html Sun Jul 05 11:55:54 2020 +0200 @@ -11,6 +11,7 @@