| 185 "--debug") BUILD_TYPE="debug" ;; |
187 "--debug") BUILD_TYPE="debug" ;; |
| 186 "--release") BUILD_TYPE="release" ;; |
188 "--release") BUILD_TYPE="release" ;; |
| 187 "--with-docs="*) OPT_WITH_DOCS=${ARG#--with-docs=} ;; |
189 "--with-docs="*) OPT_WITH_DOCS=${ARG#--with-docs=} ;; |
| 188 "--enable-coverage") FEATURE_COVERAGE=on ;; |
190 "--enable-coverage") FEATURE_COVERAGE=on ;; |
| 189 "--disable-coverage") unset FEATURE_COVERAGE ;; |
191 "--disable-coverage") unset FEATURE_COVERAGE ;; |
| |
192 "--enable-szmul-builtin") FEATURE_SZMUL_BUILTIN=on ;; |
| |
193 "--disable-szmul-builtin") unset FEATURE_SZMUL_BUILTIN ;; |
| 190 "-"*) echo "unknown option: $ARG"; abort_configure ;; |
194 "-"*) echo "unknown option: $ARG"; abort_configure ;; |
| 191 esac |
195 esac |
| 192 done |
196 done |
| 193 |
197 |
| 194 |
198 |
| 601 fi |
605 fi |
| 602 if [ -n "$DISABLE_FEATURE_COVERAGE" ]; then |
606 if [ -n "$DISABLE_FEATURE_COVERAGE" ]; then |
| 603 unset FEATURE_COVERAGE |
607 unset FEATURE_COVERAGE |
| 604 fi |
608 fi |
| 605 fi |
609 fi |
| |
610 if [ -n "$FEATURE_COVERAGE" ]; then |
| |
611 : |
| |
612 else |
| |
613 : |
| |
614 fi |
| |
615 if [ -n "$FEATURE_SZMUL_BUILTIN" ]; then |
| |
616 if [ -n "$DISABLE_FEATURE_SZMUL_BUILTIN" ]; then |
| |
617 unset FEATURE_SZMUL_BUILTIN |
| |
618 fi |
| |
619 fi |
| |
620 if [ -n "$FEATURE_SZMUL_BUILTIN" ]; then |
| |
621 : |
| |
622 else |
| |
623 : |
| |
624 TEMP_CFLAGS="$TEMP_CFLAGS -DCX_NO_SZMUL_BUILTIN" |
| |
625 TEMP_CXXFLAGS="$TEMP_CXXFLAGS -DCX_NO_SZMUL_BUILTIN" |
| |
626 fi |
| 606 |
627 |
| 607 # Option: --with-docs |
628 # Option: --with-docs |
| 608 if [ -z "$OPT_WITH_DOCS" ]; then |
629 if [ -z "$OPT_WITH_DOCS" ]; then |
| 609 echo "auto-detecting option 'with-docs'" |
630 echo "auto-detecting option 'with-docs'" |
| 610 SAVED_ERROR="$ERROR" |
631 SAVED_ERROR="$ERROR" |
| 725 if [ -n "$FEATURE_COVERAGE" ]; then |
746 if [ -n "$FEATURE_COVERAGE" ]; then |
| 726 echo " coverage: on" |
747 echo " coverage: on" |
| 727 else |
748 else |
| 728 echo " coverage: off" |
749 echo " coverage: off" |
| 729 fi |
750 fi |
| |
751 if [ -n "$FEATURE_SZMUL_BUILTIN" ]; then |
| |
752 echo " szmul-builtin: on" |
| |
753 else |
| |
754 echo " szmul-builtin: off" |
| |
755 fi |
| 730 echo |
756 echo |
| 731 |
757 |
| 732 # generate the config.mk file |
758 # generate the config.mk file |
| 733 cat > "$TEMP_DIR/config.mk" << __EOF__ |
759 cat > "$TEMP_DIR/config.mk" << __EOF__ |
| 734 # |
760 # |