When curl fails with a 404 error, don't write this error to disk

2010-04-04 14:30:29 -05:00 · 2010-04-04 14:30:29 -05:00 · f75e0eefbb
parent e70a5a8cfc
commit f75e0eefbb
1 changed files with 1 additions and 1 deletions
--- a/build-support/factor.sh
+++ b/build-support/factor.sh
@ -68,7 +68,7 @@ set_downloader() {
    if [[ $? -ne 0 ]] ; then
        DOWNLOADER=wget
    else
-        DOWNLOADER="curl -O"
+        DOWNLOADER="curl -f -O"
    fi
 }