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

diff --git a/build-support/factor.sh b/build-support/factor.sh
index 3a5fb4e253eb0819d4d28c2ee480ee42f164bb60..38bdc8183c37b24741a11148ce6bea31c421a4d7 100755 (executable)
--- 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
 }