From ec7e744cfdeb3462b13c3f27809cb4b192ea542a Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Fri, 20 Jul 2018 22:24:55 -0400
Subject: Add git diff for better debugging of C-file issues

---
 etc/ci/travis.sh | 1 +
 1 file changed, 1 insertion(+)

(limited to 'etc')

diff --git a/etc/ci/travis.sh b/etc/ci/travis.sh
index b2bac80a1..6c28b40da 100755
--- a/etc/ci/travis.sh
+++ b/etc/ci/travis.sh
@@ -14,5 +14,6 @@ python "./etc/coq-scripts/timing/make-one-time-file.py" "time-of-build.log" "tim
 rm -f "${CUR_ARCHIVE}"
 tar -czf "${CUR_ARCHIVE}" time-of-build.log src bbv coqprime || exit $?
 
+git diff
 cat time-of-build-pretty.log
 make "$@" -j2 TIMED=1 || exit $?
-- 
cgit v1.2.3