diff -r 6769a888fd3f -r 33d229634809 docs/src/header.html --- a/docs/src/header.html Mon Nov 13 13:27:18 2017 +0100 +++ b/docs/src/header.html Mon Nov 13 15:54:17 2017 +0100 @@ -34,7 +34,16 @@