diff --git a/doc/devel/index.html b/doc/devel/index.html index c8af0214ef6..b9b526b943a 100644 --- a/doc/devel/index.html +++ b/doc/devel/index.html @@ -3,5 +3,8 @@