Fixing post results

runtimeverification · Sep 21, 2023 · a2d00ed · a2d00ed
1 parent 0f27534
commit a2d00ed
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: |