From 8e029978760d6de340d7144f20b1a98a1b291058 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 23 Oct 2018 20:01:15 -0400
Subject: [travis] Always display the diff, but don't display _CoqProject

Because remove_autogenerated.sh updates _CoqProject, and we don't want
to see the churn from that.
---
 etc/ci/travis.sh | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'etc')

diff --git a/etc/ci/travis.sh b/etc/ci/travis.sh
index 981dcd7e1..8942d1db7 100755
--- a/etc/ci/travis.sh
+++ b/etc/ci/travis.sh
@@ -15,8 +15,9 @@ 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 $?
 
-if [ ! -f finished.ok ]; then
-  git diff
-fi
+git update-index --assume-unchanged _CoqProject
+git status
+git diff
+
 cat time-of-build-pretty.log
 make "$@" -j2 TIMED=1 || exit $?
-- 
cgit v1.2.3