diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 87fe7f16d..d0b834e04 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -563,8 +563,8 @@ def display_help(exit_code): if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") - print(" -f --foci2= use foci2 library at path") - print(" --noomp disable OpenMP and all features that require it.") + print(" -f --foci2= use foci2 library at path") + print(" --noomp disable OpenMP and all features that require it.") print("") print("Some influential environment variables:") if not IS_WINDOWS: