diff options
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" |