Skip to content

Commit

Permalink
List more files on github actions make
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Sep 19, 2024
1 parent 01ce421 commit 8334b84
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions etc/ci/github-actions-make.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 8334b84

Please sign in to comment.