Skip to content

Commit

Permalink
Use 4 vCPUs for running coverage-recording tests
Browse files Browse the repository at this point in the history
We changed the number of vCPUs for most scenarios in 55e5bdf, but
failed to also propagate this to coverage-recording test execution.
  • Loading branch information
tautschnig committed Jun 21, 2024
1 parent 3e5e423 commit 9fa738a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/coverage.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ jobs:
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
- name: Configure CMake CBMC build with coverage instrumentation parameters
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=2 -DCMAKE_CXX_COMPILER=/usr/bin/g++
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=${{env.linux-vcpus}} -DCMAKE_CXX_COMPILER=/usr/bin/g++
- name: Zero ccache stats and limit in size
run: ccache -z --max-size=7G
- name: Execute CMake CBMC build
Expand Down

0 comments on commit 9fa738a

Please sign in to comment.