diff --git a/.travis/docker-install.sh b/.travis/docker-install.sh index 7f405130b..f8cab10ed 100755 --- a/.travis/docker-install.sh +++ b/.travis/docker-install.sh @@ -1,5 +1,7 @@ #!/usr/bin/env bash +set -e + docker pull coqorg/coq:${COQ} docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} coqorg/coq:${COQ} docker exec COQ /bin/bash --login -c " diff --git a/.travis/docker-test.sh b/.travis/docker-test.sh index 5d173ba2d..d27b4a91d 100755 --- a/.travis/docker-test.sh +++ b/.travis/docker-test.sh @@ -1,5 +1,7 @@ #!/usr/bin/env bash +set -e + echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r' docker exec COQ /bin/bash --login -c "