diff --git a/docs/header.html b/docs/header.html
index beb85e98a7..c8cb135f55 100644
--- a/docs/header.html
+++ b/docs/header.html
@@ -15,6 +15,21 @@
td.c2 {font-family: arial, helvetica, sans-serif; font-size: 80%}
td.c1 {font-family: lucida, helvetica; font-size: 248%}
+