diff --git a/doc/header.html.in b/doc/header.html.in index 26c65b11c..9790b2d00 100644 --- a/doc/header.html.in +++ b/doc/header.html.in @@ -6,6 +6,7 @@ +