diff options
author | Michael Widenius <monty@askmonty.org> | 2012-09-22 15:30:24 +0300 |
---|---|---|
committer | Michael Widenius <monty@askmonty.org> | 2012-09-22 15:30:24 +0300 |
commit | 3e83c4e8f90851040be921443b52144a2862444a (patch) | |
tree | f76ee35018c73f2034e0e6e42c89c038f920f495 /BUILD | |
parent | 513923868545338c00390f35f63b92efd55f50bb (diff) | |
parent | 79feec77ed4a7121e68be1dc16f79dcad6c5d25e (diff) | |
download | mariadb-git-3e83c4e8f90851040be921443b52144a2862444a.tar.gz |
Automatic merge
Diffstat (limited to 'BUILD')
-rw-r--r-- | BUILD/FINISH.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/BUILD/FINISH.sh b/BUILD/FINISH.sh index 37dcd1fe836..b7ff195ccf6 100644 --- a/BUILD/FINISH.sh +++ b/BUILD/FINISH.sh @@ -21,6 +21,12 @@ extra_configs="$extra_configs $local_infile_configs $EXTRA_CONFIGS" configure="./configure $base_configs $extra_configs" +if test "$just_print" = "1" -a "$just_configure" = "1" +then + just_print="" + configure="$configure --print" +fi + commands="\ /bin/rm -rf configure; /bin/rm -rf CMakeCache.txt CMakeFiles/ |