diff --git a/docs/ProgrammersManual.html b/docs/ProgrammersManual.html index 4ce446e9189..8e9141445af 100644 --- a/docs/ProgrammersManual.html +++ b/docs/ProgrammersManual.html @@ -69,9 +69,12 @@ option