diff --git a/test/Makefile.inc b/test/Makefile.inc index 354f7a02816ae9861ea858ca2fce167d30635ce3..80fc2b8fccf2136459d6a081457997e30253180f 100644 --- a/test/Makefile.inc +++ b/test/Makefile.inc @@ -1,4 +1,4 @@ -# Time-stamp: <modified the 25/01/2023 (at 11:01) by Erwan Jahier> +# Time-stamp: <modified the 29/01/2023 (at 16:21) by Erwan Jahier> # # Define some default rules that ought to work most of the time # @@ -106,7 +106,9 @@ endif ledit -h rdbg-history -x rdbg --sasa -sut "sasa $* $(DAEMON)" -l 10000 %.rdbg-test: %.cma - rdbg --sasa -sut "sasa $*.dot $(DAEMON)" -go --input some_session -l 10000 + rdbg --sasa -sut "sasa $*.dot $(DAEMON)" -go --input some_session -l 10000 \ + | grep Error > $*.rdbg-test.log && echo "Error: 'make $@' failed" \ + && cat $*.rdbg-test.log && exit 2 || echo "'make $@' suceeds" %.rdbgui: %.cma - rdbgui4sasa -sut "sasa $*.dot $(DAEMON)" -l 10000 + ledit -h rdbg-history -x rdbgui4sasa -sut "sasa $*.dot" -l 10000