diff -r 92e482410453 -r d345541018fa docs/api-2.1/menu.js --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/docs/api-2.1/menu.js Sat Feb 06 19:11:44 2021 +0100 @@ -0,0 +1,26 @@ +function initMenu(relPath,searchEnabled,serverSide,searchPage,search) { + function makeTree(data,relPath) { + var result=''; + if ('children' in data) { + result+='