diff --git a/collects/meta/build/build b/collects/meta/build/build index 91b0140613..202f7b8727 100755 --- a/collects/meta/build/build +++ b/collects/meta/build/build @@ -1913,7 +1913,7 @@ do_installers_page_body() { # input: selector-html table-html echo " dnld_update();" echo "// -->" echo "