From 45c7fd842bd2437e831d46c31fe1ffa147f9177a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 22 Feb 2024 18:52:31 +0100 Subject: [PATCH] Another fix for the profiling workflow (#1038) --- .github/workflows/profiling.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index 6c59fcdb14..d323f1be5a 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -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