From 8334b848f72169a76ed281069822b91b581fe7cf Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 19 Sep 2024 11:26:39 -0700 Subject: [PATCH] List more files on github actions make --- etc/ci/github-actions-make.sh | 1 + 1 file changed, 1 insertion(+) 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