diff options
Diffstat (limited to 'configure.ac.pamphlet')
| -rw-r--r-- | configure.ac.pamphlet | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/configure.ac.pamphlet b/configure.ac.pamphlet index 69fdf684..db7b72f6 100644 --- a/configure.ac.pamphlet +++ b/configure.ac.pamphlet @@ -489,6 +489,16 @@ fi AC_SUBST(axiom_enable_checking) AC_SUBST(axiom_optimize_options) + +## Parse args for profiling-enabled build. +oa_enable_profiling=no +AC_ARG_ENABLE([profiling], [ --enable-profiling turn profiling on], + [case $enableval in + yes|no) oa_enable_profiling=$enableval ;; + *) AC_MSG_ERROR([erroneous value for --enable-profiling]) ;; + esac]) + +AC_SUBST(oa_enable_profiling) @ |