diff options
Diffstat (limited to 'scripts/lib/ptxd_make_get.sh')
| -rw-r--r-- | scripts/lib/ptxd_make_get.sh | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/scripts/lib/ptxd_make_get.sh b/scripts/lib/ptxd_make_get.sh index 9f869106..f28de706 100644 --- a/scripts/lib/ptxd_make_get.sh +++ b/scripts/lib/ptxd_make_get.sh @@ -78,6 +78,17 @@ Please download '${url}' manually into '${PTXDIST_SRCDIR}' EOF + set -- ${orig_argv[@]} + if [ $# -ne 1 ]; then + cat >&2 <<EOF +If this URL doesn't work, you may try these ones: +EOF + while [ ${#} -ne 0 ]; do + [ "${1}" != "${url}" ] && echo "'${1}'" >&2 + shift + done + echo + fi exit 1 fi } |