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