diff -r ec1509240080 -r 32f439d70127 docs/src/header.html --- a/docs/src/header.html Sat Dec 14 09:31:59 2019 +0100 +++ b/docs/src/header.html Sat Dec 14 09:45:39 2019 +0100 @@ -37,7 +37,7 @@