File tree Expand file tree Collapse file tree 2 files changed +4
-131
lines changed Expand file tree Collapse file tree 2 files changed +4
-131
lines changed Load Diff This file was deleted.
Original file line number Diff line number Diff line change @@ -74,7 +74,8 @@ Resources:
74
74
- echo ${Repository} > COMMIT_INFO
75
75
- git rev-parse --short HEAD >> COMMIT_INFO
76
76
- git log HEAD^..HEAD >> COMMIT_INFO
77
- - make -C src minisat2-download glucose-download
77
+ - make -C src minisat2-download glucose-download cadical-download
78
+ - sed -i 's/-Wno-error=misleading-indentation//' src/config.inc
78
79
- make -C src -j8
79
80
artifacts:
80
81
files:
@@ -116,7 +117,8 @@ Resources:
116
117
- echo ${Repository} > COMMIT_INFO
117
118
- git rev-parse --short HEAD >> COMMIT_INFO
118
119
- git log HEAD^..HEAD >> COMMIT_INFO
119
- - make -C src minisat2-download glucose-download
120
+ - make -C src minisat2-download glucose-download cadical-download
121
+ - sed -i 's/-Wno-error=misleading-indentation//' src/config.inc
120
122
- make -C src -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg"
121
123
artifacts:
122
124
files:
You can’t perform that action at this time.
0 commit comments