diff --git a/doc/head.html b/doc/head.html index 7b94f0f794..cd743b2fd1 100644 --- a/doc/head.html +++ b/doc/head.html @@ -3,6 +3,17 @@ $title + + + + +