diff options
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 74845263c9..1d9b74febc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -496,7 +496,7 @@ install-pcoq-manpages: # tests ########################################################################### -check:: world pcoq +check:: world cd test-suite; \ env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log if grep -F 'Error!' test-suite/check.log ; then false; fi |