diff options
Diffstat (limited to 'contrib/get-cryptominisat')
| -rwxr-xr-x | contrib/get-cryptominisat | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/get-cryptominisat b/contrib/get-cryptominisat index 476d1ff10..263939bcc 100755 --- a/contrib/get-cryptominisat +++ b/contrib/get-cryptominisat @@ -5,7 +5,6 @@ source "$(dirname "$0")/get-script-header.sh" CMS_DIR="$DEPS_DIR/cryptominisat5" version="5.8.0" -check_dep_dir "$CMS_DIR" setup_dep \ "https://github.com/msoos/cryptominisat/archive/$version.tar.gz" \ "$CMS_DIR" |