diff -r 7dfa5bcf39ee -r 88a9ee79c102 docs/api-2.1/menu.js --- a/docs/api-2.1/menu.js Wed Jan 22 21:02:46 2025 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -function initMenu(relPath,searchEnabled,serverSide,searchPage,search) { - function makeTree(data,relPath) { - var result=''; - if ('children' in data) { - result+='