diff --git a/doc/Section_intro.html b/doc/Section_intro.html index 36bab8fa6f..db64d2821a 100644 --- a/doc/Section_intro.html +++ b/doc/Section_intro.html @@ -140,7 +140,7 @@ commands)