diff --git a/doc/configuration.txt b/doc/configuration.txt index ece3919f0..18da6a52b 100644 --- a/doc/configuration.txt +++ b/doc/configuration.txt @@ -1919,6 +1919,40 @@ hard-stop-after