diff --git a/doc/Section_intro.html b/doc/Section_intro.html index bce1a9d718..30eea8c808 100644 --- a/doc/Section_intro.html +++ b/doc/Section_intro.html @@ -139,7 +139,7 @@ commands)