diff --git a/doc/src/Manual.txt b/doc/src/Manual.txt index fc728afd61..f8f7644e5b 100644 --- a/doc/src/Manual.txt +++ b/doc/src/Manual.txt @@ -1,7 +1,7 @@