diff --git a/doc/index.php b/doc/index.php index 59621a5d3f..104cbb401b 100644 --- a/doc/index.php +++ b/doc/index.php @@ -169,6 +169,7 @@ function show_other() {