diff options
Diffstat (limited to 'testsuite/makefiles/Makefile.several')
| -rw-r--r-- | testsuite/makefiles/Makefile.several | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/testsuite/makefiles/Makefile.several b/testsuite/makefiles/Makefile.several index 327e70997a..f22b3e6401 100644 --- a/testsuite/makefiles/Makefile.several +++ b/testsuite/makefiles/Makefile.several @@ -46,7 +46,7 @@ run-file: @if [ -f `basename $(FILE) ml`checker ]; then \ sh `basename $(FILE) ml`checker; \ else \ - diff -q `basename $(FILE) ml`reference `basename $(FILE) ml`result > /dev/null || (echo " => failed" && exit 1); \ + $(DIFF) `basename $(FILE) ml`reference `basename $(FILE) ml`result > /dev/null || (echo " => failed" && exit 1); \ fi promote: defaultpromote |