diff --git a/Doc/tools/mkmodindex b/Doc/tools/mkmodindex index 14568d129ea..45c7485b012 100755 --- a/Doc/tools/mkmodindex +++ b/Doc/tools/mkmodindex @@ -161,53 +161,53 @@ platform they are available on.