diff options
Diffstat (limited to 'configure.src')
| -rw-r--r-- | configure.src | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/configure.src b/configure.src index 889902eb96..4b748f2545 100644 --- a/configure.src +++ b/configure.src @@ -70,8 +70,10 @@ while test $# != 0; do ERL_TOP="$user_srcdir" ;; --enable-bootstrap-only) + config_arguments="$config_arguments --enable-bootstrap-only" bootstrap_only=yes;; --disable-bootstrap-only) + config_arguments="$config_arguments --disable-bootstrap-only" bootstrap_only=no;; --enable-option-checking) echo "ERROR: Cannot enable option checking" 1>&2 |