File tree Expand file tree Collapse file tree 2 files changed +2
-131
lines changed Expand file tree Collapse file tree 2 files changed +2
-131
lines changed Load Diff This file was deleted.
Original file line number Diff line number Diff line change @@ -74,7 +74,7 @@ Resources:
7474 - echo ${Repository} > COMMIT_INFO
7575 - git rev-parse --short HEAD >> COMMIT_INFO
7676 - git log HEAD^..HEAD >> COMMIT_INFO
77- - make -C src minisat2-download glucose-download
77+ - make -C src minisat2-download glucose-download cadical-download
7878 - make -C src -j8
7979 artifacts:
8080 files:
@@ -116,7 +116,7 @@ Resources:
116116 - echo ${Repository} > COMMIT_INFO
117117 - git rev-parse --short HEAD >> COMMIT_INFO
118118 - git log HEAD^..HEAD >> COMMIT_INFO
119- - make -C src minisat2-download glucose-download
119+ - make -C src minisat2-download glucose-download cadical-download
120120 - make -C src -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg"
121121 artifacts:
122122 files:
You can’t perform that action at this time.
0 commit comments