diff --git a/docs/user/header.html b/docs/user/header.html index 8565f097ae..2c0fe5b34d 100644 --- a/docs/user/header.html +++ b/docs/user/header.html @@ -7,6 +7,6 @@