diff --git a/collects/meta/build/build b/collects/meta/build/build index 060abc2e49..50b7702829 100755 --- a/collects/meta/build/build +++ b/collects/meta/build/build @@ -2114,8 +2114,6 @@ BUILD_PRE_WEB() { move_from_maindir "$docdir" html_file_row "$docdir" "Documentation files" #---- - html_file_row "search.html" "Search the current sources and docs" - #---- move_from_maindir "$bindir" html_file_row "$bindir" "Platform-specific binary files" #----