diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-02-12 08:49:50 -0500 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-02-12 08:49:50 -0500 |
| commit | 3ba153b4be4c2fe8ad7decf8ebc7cf5d8815a0e9 (patch) | |
| tree | 8d0070c3064d471b91b098bdffcd08a78a890632 | |
| parent | 6ecdf49ae2a75c76fc8d37c7d396cc777b2e3adf (diff) | |
try curl before wget, workaround for issue with FTP PASV
| -rwxr-xr-x | contrib/get-antlr-3.4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 index 74bce743e..436ef6a8d 100755 --- a/contrib/get-antlr-3.4 +++ b/contrib/get-antlr-3.4 @@ -15,10 +15,10 @@ if ! [ -e src/parser/cvc/Cvc.g ]; then fi function webget { - if which wget &>/dev/null; then - wget -c -O "$2" "$1" - elif which curl &>/dev/null; then + if which curl &>/dev/null; then curl "$1" >"$2" + elif which wget &>/dev/null; then + wget -c -O "$2" "$1" else echo "Can't figure out how to download from web. Please install wget or curl." >&2 exit 1 |