diff --git a/doc/Section_intro.html b/doc/Section_intro.html index 90e12308ba..a290ab4d1d 100644 --- a/doc/Section_intro.html +++ b/doc/Section_intro.html @@ -122,7 +122,7 @@ commands)