From 05006114c3843b3e87c9cecaf1b6ece34c3843c2 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 22 Mar 2018 02:22:03 -0400
Subject: Die early if we can't create the archive

This would have caught the issue fixed by the previous commit much earlier.
---
 etc/ci/travis.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'etc')

diff --git a/etc/ci/travis.sh b/etc/ci/travis.sh
index 6c2971685..b2bac80a1 100755
--- a/etc/ci/travis.sh
+++ b/etc/ci/travis.sh
@@ -12,7 +12,7 @@ mkdir -p "${CACHE_DIR}"
 make "$@" -j2 TIMED=1 2>&1 | tee -a time-of-build.log
 python "./etc/coq-scripts/timing/make-one-time-file.py" "time-of-build.log" "time-of-build-pretty.log" || exit $?
 rm -f "${CUR_ARCHIVE}"
-tar -czf "${CUR_ARCHIVE}" time-of-build.log src bbv coqprime
+tar -czf "${CUR_ARCHIVE}" time-of-build.log src bbv coqprime || exit $?
 
 cat time-of-build-pretty.log
 make "$@" -j2 TIMED=1 || exit $?
-- 
cgit v1.2.3