diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-14 08:24:33 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-14 08:24:33 -0700 |
| commit | f5a823ba45f9def7effe3d03585a881bc90bb0ad (patch) | |
| tree | 32d8ad6a51091680d802890d1894e485b8ca9f56 /config | |
| parent | 94e3d283a58684118e06f9a698606e58574fa26f (diff) | |
autotools: Remove personal builds, rename build 'default' to 'testing'. (#2303)
Diffstat (limited to 'config')
| -rw-r--r-- | config/cvc4.m4 | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 1b0e88098..c6d19a3ea 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -49,7 +49,7 @@ handle_option() { ;; -*|*=*) ;; - production|production-*|debug|debug-*|competition|competition-*) + production|production-*|debug|debug-*|competition|competition-*|testing|testing-*) # regexp `\?' not supported on Mac OS X ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'` ac_cvc4_build_profile_set=yes @@ -103,18 +103,7 @@ handle_option() { unset ac_cvc4_rewritten_args for ac_option do - if test "$ac_option" = personal; then - if test -e personal.conf; then - handle_option --enable-personal-make-rules - while read arg; do - handle_option "$arg" - done < personal.conf - else - AC_MSG_ERROR([personal build profile selected, but cannot find personal.conf]) - fi - else - handle_option "$ac_option" - fi + handle_option "$ac_option" done eval set x $ac_cvc4_rewritten_args shift |