Skip to content

Commit

Permalink
fewer checkouts
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed May 16, 2024
1 parent f7d2915 commit ffef9ed
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions .github/workflows/ml_stats_label.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,9 @@ jobs:
- id: mathlib_stats
run: |
git checkout adomani/periodic_reports_dev
#git checkout -q master
#git checkout adomani/periodic_reports_dev
git checkout -q master
git checkout origin/adomani/periodic_reports_dev scripts/mathlib_stats.sh
## should the next step be removed for Zulip?
#git checkout -q -
printf $'summary<<EOF\n%s\nEOF' "$(./scripts/mathlib_stats.sh)"
Expand Down

0 comments on commit ffef9ed

Please sign in to comment.