diff --git a/docs/manual.html b/docs/manual.html index ff542bf6..cdafd903 100644 --- a/docs/manual.html +++ b/docs/manual.html @@ -6272,7 +6272,7 @@