diff --git a/doc/header.html b/doc/header.html index 55f2ea171c..bbaf1d53b4 100644 --- a/doc/header.html +++ b/doc/header.html @@ -22,6 +22,7 @@ $extrastylesheet