diff --git a/doc/Section_intro.html b/doc/Section_intro.html index 173180c3a2..77df3ae706 100644 --- a/doc/Section_intro.html +++ b/doc/Section_intro.html @@ -144,7 +144,7 @@ commands)