diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh index 1ac34a0ab6..210872b92d 100755 --- a/etc/ci/github-actions-make.sh +++ b/etc/ci/github-actions-make.sh @@ -54,6 +54,7 @@ rm -f finished.ok python "./etc/coq-scripts/timing/make-one-time-file.py" ${make_one_time_file_real} "time-of-build.log" "time-of-build-pretty.log" || exit $? git status +git ls-files --others --exclude-standard git diff cat time-of-build-pretty.log