diff --git a/docs/ProgrammersManual.html b/docs/ProgrammersManual.html index e6349b1ec82..9d007566c96 100644 --- a/docs/ProgrammersManual.html +++ b/docs/ProgrammersManual.html @@ -3298,7 +3298,7 @@ simplifies the representation and makes it easier to manipulate.