diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-01-09 16:48:32 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-01-09 16:48:32 -0500 |
| commit | 780448ae48ed8755b11570a6843ab6871d94abef (patch) | |
| tree | f2d742331c01324eb53208412e5b640a7cc86996 /config | |
| parent | 15c807ff344a5042604e83b975de4937ac7c309d (diff) | |
| parent | 1e5d35f3867744a5c793985a9a31cdd6149750b7 (diff) | |
Merge branch '1.3.x'
Diffstat (limited to 'config')
| -rwxr-xr-x | config/build-type | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/config/build-type b/config/build-type index f5ea50bde..1ef9191f7 100755 --- a/config/build-type +++ b/config/build-type @@ -31,7 +31,7 @@ # profiling # # Also you can specify "cln" or "gmp". If "gmp", the build dir -# contains the string "gmp". (cln is considered the default.) +# contains the string "gmp". (gmp is considered the default.) # # Also for glpk. # @@ -46,8 +46,8 @@ shift while [ $# -gt 0 ]; do case "$1" in - cln) ;; - gmp) gmp=1 ;; + cln) cln=1 ;; + gmp) ;; no*) eval `expr "$1" : 'no\(.*\)'`=0 ;; *) eval $1=1 ;; esac @@ -55,7 +55,7 @@ while [ $# -gt 0 ]; do done build_type_suffix= -for arg in gmp glpk staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do +for arg in cln glpk staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do if eval [ -n '"${'$arg'+set}"' ]; then if eval [ '"${'$arg'}"' -eq 0 ]; then build_type_suffix=$build_type_suffix-no$arg |