Skip to content

Commit

Permalink
Use -p option of test.pl instead of printer script
Browse files Browse the repository at this point in the history
This script was removed, so mentions of it in Makefiles need to be
replaced by usage of -p option of test.pl.
  • Loading branch information
romainbrenguier committed Nov 24, 2017
1 parent 1821b1a commit a6af95d
Showing 1 changed file with 4 additions and 16 deletions.
20 changes: 4 additions & 16 deletions regression/jbmc-strings/Makefile
Original file line number Diff line number Diff line change
@@ -1,28 +1,16 @@
default: tests.log

test:
@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
../failed-tests-printer.pl ; \
exit 1 ; \
fi
@../test.pl -p -c ../../../src/jbmc/jbmc

testfuture:
@if ! ../test.pl -c ../../../src/jbmc/jbmc -CF ; then \
../failed-tests-printer.pl ; \
exit 1 ; \
fi
@../test.pl -p -c ../../../src/jbmc/jbmc -CF

testall:
@if ! ../test.pl -c ../../../src/jbmc/jbmc -CFTK ; then \
../failed-tests-printer.pl ; \
exit 1 ; \
fi
@../test.pl -p -c ../../../src/jbmc/jbmc -CFTK

tests.log: ../test.pl
@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
../failed-tests-printer.pl ; \
exit 1 ; \
fi
@../test.pl -p -c ../../../src/jbmc/jbmc

show:
@for dir in *; do \
Expand Down

0 comments on commit a6af95d

Please sign in to comment.