diff -r 92e482410453 -r d345541018fa docs/src/header.html --- a/docs/src/header.html Mon Dec 30 09:54:10 2019 +0100 +++ b/docs/src/header.html Sat Feb 06 19:11:44 2021 +0100 @@ -18,24 +18,9 @@