diff --git a/doc/formats/html/html_changes/menu.js b/doc/formats/html/html_changes/menu.js index 9b399756a..670f059d4 100644 --- a/doc/formats/html/html_changes/menu.js +++ b/doc/formats/html/html_changes/menu.js @@ -5,9 +5,32 @@ function initMenu(relPath,searchEnabled,serverSide,searchPage,search) { result+='