File tree 1 file changed +2
-2
lines changed
1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -201,7 +201,7 @@ jobs:
201
201
- cmake --build build -- -j4
202
202
script : (cd build; bin/unit "[core][irept]")
203
203
204
- # cmake build using g++-7, enable CMAKE_USE_CUDD
204
+ # cmake build using g++-7, enable CMAKE_USE_CUDD and BDD_GUARDS
205
205
- stage : Test different OS/CXX/Flags
206
206
os : linux
207
207
sudo : false
@@ -223,7 +223,7 @@ jobs:
223
223
install :
224
224
- ccache -z
225
225
- ccache --max-size=1G
226
- - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true'
226
+ - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
227
227
- git submodule update --init --recursive
228
228
- cmake --build build -- -j4
229
229
script : (cd build; ctest -V -L CORE -j2)
You can’t perform that action at this time.
0 commit comments