File tree 1 file changed +4
-16
lines changed
1 file changed +4
-16
lines changed Original file line number Diff line number Diff line change 1
1
default : tests.log
2
2
3
3
test :
4
- @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
5
- ../failed-tests-printer.pl ; \
6
- exit 1 ; \
7
- fi
4
+ @../test.pl -p -c ../../../src/jbmc/jbmc
8
5
9
6
testfuture :
10
- @if ! ../test.pl -c ../../../src/jbmc/jbmc -CF ; then \
11
- ../failed-tests-printer.pl ; \
12
- exit 1 ; \
13
- fi
7
+ @../test.pl -p -c ../../../src/jbmc/jbmc -CF
14
8
15
9
testall :
16
- @if ! ../test.pl -c ../../../src/jbmc/jbmc -CFTK ; then \
17
- ../failed-tests-printer.pl ; \
18
- exit 1 ; \
19
- fi
10
+ @../test.pl -p -c ../../../src/jbmc/jbmc -CFTK
20
11
21
12
tests.log : ../test.pl
22
- @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
23
- ../failed-tests-printer.pl ; \
24
- exit 1 ; \
25
- fi
13
+ @../test.pl -p -c ../../../src/jbmc/jbmc
26
14
27
15
show :
28
16
@for dir in * ; do \
You can’t perform that action at this time.
0 commit comments