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-gmp-dev | |
| 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-gmp-dev')
| -rwxr-xr-x | contrib/get-gmp-dev | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/contrib/get-gmp-dev b/contrib/get-gmp-dev index ef2023d04..3fc913a7d 100755 --- a/contrib/get-gmp-dev +++ b/contrib/get-gmp-dev @@ -17,8 +17,6 @@ source "$(dirname "$0")/get-script-header.sh" GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION" -check_dep_dir "$GMP_DIR" - echo ============================================================================= echo echo "This script should only be used if your distribution does not ship with the" |