diff --git a/doc/header.html b/doc/header.html index e212a83cb..e175de778 100644 --- a/doc/header.html +++ b/doc/header.html @@ -51,7 +51,7 @@