diff --git a/Doc/tools/mkmodindex b/Doc/tools/mkmodindex index 20c6416abd1..4400cea5719 100755 --- a/Doc/tools/mkmodindex +++ b/Doc/tools/mkmodindex @@ -166,8 +166,10 @@ NAVIGATION = """\