diff --git a/documentation/ref-manual/ref-varlocality.xml b/documentation/ref-manual/ref-varlocality.xml index 49d9a2dc68..145b572145 100644 --- a/documentation/ref-manual/ref-varlocality.xml +++ b/documentation/ref-manual/ref-varlocality.xml @@ -82,7 +82,7 @@