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