Skip to content

Commit

Permalink
Another fix for the profiling workflow (#1038)
Browse files Browse the repository at this point in the history
  • Loading branch information
fredrik-bakke authored Feb 22, 2024
1 parent d4d3e8b commit 45c7fd8
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/profiling.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ jobs:
mkdir benchmark-cache
curl 'https://agda-unimath-benchmarks.netlify.app/data.json' -o benchmark-cache/data.json
# Stop if there is no initial data (the server gave us an HTML instead of a JSON)
(head -1 benchmark-cache/data.json | grep -v DOCTYPE) || (rm benchmark-cache/data.json; exit 0)
(head -1 benchmark-cache/data.json | grep -v DOCTYPE) || {rm benchmark-cache/data.json; exit 0}
curl 'https://agda-unimath-benchmarks.netlify.app/data.csv' -o benchmark-cache/data.csv
- name: Process new profiling data
Expand Down

0 comments on commit 45c7fd8

Please sign in to comment.