diff --git a/doc/Section_intro.html b/doc/Section_intro.html index 93db0021d1..f05ae1c1c3 100644 --- a/doc/Section_intro.html +++ b/doc/Section_intro.html @@ -206,6 +206,7 @@ commands)