diff --git a/doc/index.html b/doc/index.html index 83ffef54..725c74e2 100644 --- a/doc/index.html +++ b/doc/index.html @@ -14663,7 +14663,7 @@
AllocationType of this machine