Skip to content

Commit

Permalink
Get rid of dead code in gh-actions make
Browse files Browse the repository at this point in the history
_CoqProject is now generated
  • Loading branch information
JasonGross committed May 26, 2021
1 parent 3e81b29 commit 94919dc
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion etc/ci/github-actions-make.sh
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ rm -f finished.ok
(make "$@" ${OUTPUT_SYNC} TIMED=1 TIMING=1 "${reportify}" 2>&1 && touch finished.ok) | tee -a time-of-build.log
python "./etc/coq-scripts/timing/make-one-time-file.py" "time-of-build.log" "time-of-build-pretty.log" || exit $?

git update-index --assume-unchanged _CoqProject
git status
git diff

Expand Down

0 comments on commit 94919dc

Please sign in to comment.