diff --git a/doc/src/Manual.txt b/doc/src/Manual.txt index 471d3e48f4..9215d0e614 100644 --- a/doc/src/Manual.txt +++ b/doc/src/Manual.txt @@ -1,7 +1,7 @@