diff options
author | Michael Widenius <monty@askmonty.org> | 2012-09-22 17:11:40 +0300 |
---|---|---|
committer | Michael Widenius <monty@askmonty.org> | 2012-09-22 17:11:40 +0300 |
commit | 620d14f8c3521f9ec7283b8690e0e16434739d33 (patch) | |
tree | b3438fd90e14b3be2ec21e53cca37cd795090a00 /BUILD | |
parent | 288eeb3a31e4bfb52180f3906a4d354ac9cc457e (diff) | |
parent | 3e83c4e8f90851040be921443b52144a2862444a (diff) | |
download | mariadb-git-620d14f8c3521f9ec7283b8690e0e16434739d33.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/ |