diff options
author | Simon Warta <[email protected]> | 2017-04-23 09:25:51 +0200 |
---|---|---|
committer | Simon Warta <[email protected]> | 2017-04-25 00:38:04 +0200 |
commit | 3bbddc7b163e14bf37b766871bcf786a4ed6da3c (patch) | |
tree | ed614d15faa591ffe2b3818c6f4d592334209b7f /configure.py | |
parent | 868f96c02ab60d5a7b3272f1b9a5c8e5bb7a1358 (diff) |
Extract set_defaults_for_unset_options
Diffstat (limited to 'configure.py')
-rwxr-xr-x | configure.py | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/configure.py b/configure.py index 7df933b01..2c5ada573 100755 --- a/configure.py +++ b/configure.py @@ -2574,6 +2574,16 @@ def robust_makedirs(directory, max_retries=5): os.makedirs(directory) +# This is for otions that have --with-XYZ and --without-XYZ. If user does not +# set any of those, we choose a default here. +# Mutates `options` +def set_defaults_for_unset_options(options): + if options.with_sphinx is None: + if have_program('sphinx-build'): + logging.info('Found sphinx-build (use --without-sphinx to disable)') + options.with_sphinx = True + + # Checks user options for consistency # This method DOES NOT change options on behalf of the user but explains # why the given configuration does not work. @@ -2721,11 +2731,7 @@ def main(argv=None): logging.error("Unknown module set %s", options.module_policy) module_policy = module_policies[options.module_policy] - if options.with_sphinx is None: - if have_program('sphinx-build'): - logging.info('Found sphinx-build (use --without-sphinx to disable)') - options.with_sphinx = True - + set_defaults_for_unset_options(options) validate_options(options) if options.build_shared_lib and not osinfo.building_shared_supported: |