diff --git a/doc/Section_intro.html b/doc/Section_intro.html index 389ab3a627..d33a654c4f 100644 --- a/doc/Section_intro.html +++ b/doc/Section_intro.html @@ -137,7 +137,7 @@ commands)