diff --git a/docs/index.html b/docs/index.html index 8d18bfaec..edabd5f8c 100644 --- a/docs/index.html +++ b/docs/index.html @@ -473,5 +473,5 @@ diff --git a/docs/manual/tools/index.html b/docs/manual/tools/index.html index f7c7c372e..c80f72b5d 100644 --- a/docs/manual/tools/index.html +++ b/docs/manual/tools/index.html @@ -410,6 +410,10 @@ + +