diff -r 33d229634809 -r f4789572c9d6 docs/src/header.html --- a/docs/src/header.html Mon Nov 13 15:54:17 2017 +0100 +++ b/docs/src/header.html Mon Nov 20 16:10:23 2017 +0100 @@ -34,22 +34,12 @@