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-glpk-cut-log | |
| 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-glpk-cut-log')
| -rwxr-xr-x | contrib/get-glpk-cut-log | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log index 17ace0dcd..f8eff85bb 100755 --- a/contrib/get-glpk-cut-log +++ b/contrib/get-glpk-cut-log @@ -12,7 +12,6 @@ patch_file=${contrib_dir}/glpk-cut-log.patch GLPK_DIR="$DEPS_DIR/glpk-cut-log" version="4.52" -check_dep_dir "$GLPK_DIR" setup_dep \ "https://ftp.gnu.org/gnu/glpk/glpk-${version}.tar.gz" \ "$GLPK_DIR" |