diff --git a/docs/manual.html b/docs/manual.html index 77c4cc444..298398c27 100644 --- a/docs/manual.html +++ b/docs/manual.html @@ -218,7 +218,8 @@ the session, it conta