diff --git a/doc/misc/header.html b/doc/misc/header.html index d43f2aaff..2dbe72146 100644 --- a/doc/misc/header.html +++ b/doc/misc/header.html @@ -16,15 +16,6 @@ $extrastylesheet -