diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-11-02 14:10:34 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-02 14:10:34 -0800 |
| commit | 5eb06a56099612e96303429fd8a9158ed8ad3121 (patch) | |
| tree | 770676e811afa252ef45e8e5ff4aa8ede78259ac /contrib/get-script-header.sh | |
| parent | 457b0fe003c8192e35df48cfb3528b9aefe2fd1b (diff) | |
contrib: Remove dependency directories. (#5367)
This automatically removes dependency directories for scripts that get
external dependencies instead of aborting with an error.
Diffstat (limited to 'contrib/get-script-header.sh')
| -rw-r--r-- | contrib/get-script-header.sh | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh index 7a88b3be2..64ef54401 100644 --- a/contrib/get-script-header.sh +++ b/contrib/get-script-header.sh @@ -50,6 +50,7 @@ function setup_dep url="$1" directory="$2" echo "Setting up $directory ..." + rm -rf "$directory" mkdir -p "$directory" cd "$directory" webget "$url" archive @@ -57,15 +58,6 @@ function setup_dep rm archive } -function check_dep_dir -{ - if [ -e "$1" ]; then - echo "error: file or directory '$1' exists; please move it out of the way." >&2 - exit 1 - fi -} - - # Some of our dependencies do not provide a make install rule. Use the # following helper functions to copy libraries/headers/binaries into the # corresponding directories in deps/install. |