summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <noetzli@stanford.edu>2017-10-30 00:20:22 -0700
committerAndres Noetzli <noetzli@stanford.edu>2017-10-30 00:20:22 -0700
commit9d651eb93d59d5e6af190e5d68ca9d27b7081b59 (patch)
treeab534a1633161512583efe4345d6879115360d9b
parent18b4bf1c63bf311ce9ad9cdb342f5588147e55f3 (diff)
remove exitwin_deps_tmp
-rwxr-xr-xcontrib/get-win-dependencies1
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies
index efa0729e9..2342a09ff 100755
--- a/contrib/get-win-dependencies
+++ b/contrib/get-win-dependencies
@@ -74,7 +74,6 @@ echo
MACHINE_TYPE="x86_64" ANTLR_CONFIGURE_ARGS="--host=$HOST" contrib/get-antlr-3.4 | grep -v 'Now configure CVC4 with' | grep -v '\./configure --with-antlr-dir='
[ ${PIPESTATUS[0]} -eq 0 ] || reporterror
echo
-exit 0
echo =============================================================================
echo
echo "Setting up GMP $GMPVERSION..."
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback