File tree Expand file tree Collapse file tree 1 file changed +8
-0
lines changed
Expand file tree Collapse file tree 1 file changed +8
-0
lines changed Original file line number Diff line number Diff line change @@ -729,6 +729,10 @@ jobs:
729729 echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
730730 - name : Configure with cmake
731731 run : cmake -S . -B build
732+ - name : Zero ccache stats and limit in size (2 GB)
733+ run : |
734+ clcache -z
735+ clcache -M 2147483648
732736 - name : Build Release
733737 run : cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
734738 - name : Print ccache stats
@@ -789,6 +793,10 @@ jobs:
789793 run : |
790794 echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
791795 echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
796+ - name : Zero ccache stats and limit in size (2 GB)
797+ run : |
798+ clcache -z
799+ clcache -M 2147483648
792800 - name : Download minisat with make
793801 run : make -C src minisat2-download
794802 - name : Build CBMC with make
You can’t perform that action at this time.
0 commit comments