diff --git a/collects/meta/build/build b/collects/meta/build/build index 750fd03bde..be0284b422 100755 --- a/collects/meta/build/build +++ b/collects/meta/build/build @@ -2016,7 +2016,7 @@ BUILD_WEB() { separator "Making web content -- not distributing" fi GIT_DIR="$maindir/$cleandir/.git" \ - KNOWN_MIRRORS_FILE="$maindir/$knownmirrors" + KNOWN_MIRRORS_FILE="$maindir/$knownmirrors" \ _run "$PLTHOME/$webscript" $webflags }