wget -O is supposed to work like kind of shell redirect, so in case of failure 0...

Changed files:
    builder.sh -> 1.595

diff --git a/builder.sh b/builder.sh
index 64e9d5148d4ea09f42196f7fbc2f796c3174c77c..8a7cb1c01cf8143dedc74fec78f416dad20d7b4f 100644 (file)
--- a/builder.sh
+++ b/builder.sh
@@ -1073,6 +1073,7 @@ get_files() {
                                                                update_shell_title "${GETURI2%% *}: $url_attic"
                                                                ${GETURI2} ${OUTFILEOPT} "$target" "$url_attic"
                                                        fi
+                                                       test -s "$target" || rm -f "$target"
                                                fi
                                        fi
 
@@ -1104,6 +1105,7 @@ get_files() {
                                                update_shell_title "${GETURI2%% *}: $im"
                                                ${GETURI2} "$im" ${OUTFILEOPT} "$target"
                                        fi
+                                       test -s "$target" || rm -f "$target"
                                fi
 
                                if [ "$cvsup" = 1 ]; then