diff --git a/user_doc.head.html b/user_doc.head.html index 129305ea0..5c91918b4 100644 --- a/user_doc.head.html +++ b/user_doc.head.html @@ -2,6 +2,19 @@