diff --git a/doc/src/Manual.txt b/doc/src/Manual.txt index 8f5d5ed7d1..1d1357d4bd 100644 --- a/doc/src/Manual.txt +++ b/doc/src/Manual.txt @@ -1,7 +1,7 @@