File tree Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -415,10 +415,10 @@ jobs:
415415 find ${{ env.SCRATCHDIR }}/globs-job -type f -! -empty -name '*.glob.std*' > globs-job
416416 find ${{ env.SCRATCHDIR }}/globs-base -type f -! -empty -name '*.glob.std*' > globs-base
417417 (dune exec -- coqc-perf.code-quality-diff \
418- --before-globs-from-file= globs-base \
419- --after-globs-from-file= globs-job \
420- --before-dune= ${{ env.SCRATCHDIR }}/dune-log-base.json \
421- --after-dune= ${{ env.SCRATCHDIR }}/dune-log-job.json \
418+ --before-globs-from-file globs-base \
419+ --after-globs-from-file globs-job \
420+ --before-dune ${{ env.SCRATCHDIR }}/dune-log-base.json \
421+ --after-dune ${{ env.SCRATCHDIR }}/dune-log-job.json \
422422 >> $GITHUB_STEP_SUMMARY) \
423423 || true
424424 echo -e "\n" >> $GITHUB_STEP_SUMMARY
You can’t perform that action at this time.
0 commit comments