diff --git a/collects/meta/build/build b/collects/meta/build/build index 4b3dd0c05a..b0a22ed672 100755 --- a/collects/meta/build/build +++ b/collects/meta/build/build @@ -1056,7 +1056,7 @@ MAIN_BUILD() { fi if is_yes make_bins; then - header "Creating archive" + header -s "Creating archive" _cd "$maindir" _rm "$repotgz" _cd "$maindir/$cleandir" @@ -2186,9 +2186,11 @@ BUILD_PRE_WEB() { local target="$maindir/$prewebdir/$(basename "$statusscript")" { echo "#!/bin/bash" - local v - for v in tmpdir lockfile statusfile statusfile_last bglogfile; do - echo "$v=$(eval "\$$var")" + echo "" + local var + for var in tmpdir lockfile statusfile statusfile_last bglogfile; do + local val; eval val="\$$var" + echo "$var=\$$val" done echo "" cat "$PLTHOME/$statusscript" diff --git a/collects/meta/build/current-build-status.cgi b/collects/meta/build/current-build-status.cgi index c11adcc9de..a46cf9438e 100644 --- a/collects/meta/build/current-build-status.cgi +++ b/collects/meta/build/current-build-status.cgi @@ -7,7 +7,7 @@ printf 'Content-type: text/plain\r\n\r\n' # cache status reports (avoids excessive work during builds) # use a lockfile as a cheap hack to time cache refreshing -if ! lockfile -r 0 -l 5 -s 0 "$cachelock" >& /dev/null \ +if ! lockfile -r 0 -l 30 -s 0 "$cachelock" >& /dev/null \ && [[ -e "$cache" ]]; then cat "$cache"; exit fi