diff --git a/doc/Section_intro.html b/doc/Section_intro.html index afc3c5d040..bced87e8c1 100644 --- a/doc/Section_intro.html +++ b/doc/Section_intro.html @@ -139,7 +139,7 @@ commands)