diff options
Diffstat (limited to 'BUILD/SETUP.sh')
| -rw-r--r-- | BUILD/SETUP.sh | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/BUILD/SETUP.sh b/BUILD/SETUP.sh index 9c267589ad6..7e0810dfd1c 100644 --- a/BUILD/SETUP.sh +++ b/BUILD/SETUP.sh @@ -5,18 +5,25 @@ then fi nonono= -case "$1" in --n | --just-print ) nonono=1; shift ;; --h | --help ) cat <<EOF; exit 0 ;; +just_configure= +while test $# -gt 0 +do + case "$1" in + -c | --just-configure ) just_configure=1; shift ;; + -n | --just-print ) nonono=1; shift ;; + -h | --help ) cat <<EOF; exit 0 ;; Usage: $0 [-h|-n] [configure-options] -h, --help Show this help message. -n, --just-print Don't actually run any commands; just print them. + -c, --just-configure Stop after running configure. Any other options will be passed directly to configure. Note: this script is intended for internal use by MySQL developers. EOF -esac + * ) break ;; + esac +done set -e |