Fixing bencher posting command

runtimeverification · Sep 21, 2023 · 3ece2c5 · 3ece2c5
1 parent a2d00ed
commit 3ece2c5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/develop.yml b/.github/workflows/develop.yml
@@ -86,7 +86,7 @@ jobs:
           docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c 'bencher run            \
             --if-branch "develop" --else-if-branch "master"                    \
             --file .profiling-results.json --err --ci-only-on-alert            \
-            --github-actions "${GITHUB_TOKEN}" \'echo "Exporting report"\''
+            --github-actions "${GITHUB_TOKEN}" "echo \"Exporting report\"'
       - name: 'Tear down Docker'
         if: always()
         run: |