diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-15 00:24:32 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-15 00:24:32 +0100 |
commit | 2cefd431ec3371e3232a370632a4bef0569c7cd9 (patch) | |
tree | 9553583b22d1175d84bfaa91099a60d2ff5b6c37 | |
parent | 44d0d9bc1f93da603b8e14c9499e086e220f4694 (diff) | |
download | klee-2cefd431ec3371e3232a370632a4bef0569c7cd9.tar.gz |
Capture STP build output to file and only show its contents if there
is a build failure. This is so the output shown in the TravisCI web interface is kept small.
-rwxr-xr-x | .travis/stp.sh | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/.travis/stp.sh b/.travis/stp.sh index 94bbab4d..abc4e566 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -3,6 +3,8 @@ # Make sure we exit if there is a failure set -e +STP_LOG="$(pwd)/stp-build.log" + if [ "${STP_VERSION}" == "UPSTREAM" ]; then git clone --depth 1 git://github.com/stp/stp.git src mkdir build @@ -10,7 +12,10 @@ if [ "${STP_VERSION}" == "UPSTREAM" ]; then # Disabling building of shared libs is a workaround cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF ../src # Don't try to build stp executable, there's an issue with using gcc4.8 with boost libraries built with gcc4.6 - make libstp CopyPublicHeaders + + set +e # Do not exit if build fails because we need to display the log + make libstp CopyPublicHeaders >> "${STP_LOG}" 2>&1 + elif [ "${STP_VERSION}" == "r940" ]; then # Building the old "r940" version that for some reason we love so much! git clone git://github.com/stp/stp.git src_build @@ -33,8 +38,16 @@ elif [ "${STP_VERSION}" == "r940" ]; then export CXX=g++ ./scripts/configure --with-prefix=${BUILD_DIR}/stp/build --with-cryptominisat2 echo "WARNING FORCING GCC TO BE USED TO COMPILE STP" - make OPTIMIZE=-O2 CFLAGS_M32= install + + set +e # Do not exit if build fails because we need to display the log + make OPTIMIZE=-O2 CFLAGS_M32= install >> "${STP_LOG}" 2>&1 else echo "Unsupported STP_VERSION" exit 1 fi + +# Only show build output if something went wrong to keep log output short +if [ $? -ne 0 ]; then + echo "Build error" + cat "${STP_LOG}" +fi |