summaryrefslogtreecommitdiff
path: root/contrib/get-glpk-cut-log
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2018-10-19 14:45:42 -0700
committerGitHub <noreply@github.com>2018-10-19 14:45:42 -0700
commitce8c429281fd1f7e4ac4d2b7133152c1d370df0c (patch)
tree407400e728621cc9a5262e7112a93bd6acd0835a /contrib/get-glpk-cut-log
parent7de0540252b62080ee9f98617f5718cb1ae08579 (diff)
Remove autotools build system. (#2639)
Diffstat (limited to 'contrib/get-glpk-cut-log')
-rwxr-xr-xcontrib/get-glpk-cut-log2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log
index 419fdba90..dcd5aac00 100755
--- a/contrib/get-glpk-cut-log
+++ b/contrib/get-glpk-cut-log
@@ -31,4 +31,4 @@ cd ..
echo
echo ===================== Now configure CVC4 with =====================
-echo ./configure --enable-gpl --with-glpk --with-glpk-dir=`pwd`
+echo ./configure.sh --gpl --glpk
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback