aboutsummaryrefslogtreecommitdiffstats
path: root/test/c/Makefile
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-08-21 14:54:25 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-08-21 14:59:38 +0200
commit78808873d889608ee39fb6a9d9c0dac0335ccf47 (patch)
treed6d73f06b2c31abbd4028f39f143ace3459458e1 /test/c/Makefile
parent54f97d1988f623ba7422e13a504caeb5701ba93c (diff)
parentc6567a3f0a16050fd04469fdcc7a575f81c0c8f4 (diff)
downloadcompcert-78808873d889608ee39fb6a9d9c0dac0335ccf47.tar.gz
compcert-78808873d889608ee39fb6a9d9c0dac0335ccf47.zip
Merge branch 'master' into 'new-builtins'
Diffstat (limited to 'test/c/Makefile')
-rw-r--r--test/c/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/c/Makefile b/test/c/Makefile
index a81a9d5c..59a0d834 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -38,7 +38,7 @@ test:
@for i in $(PROGS); do \
if ./$$i.compcert | cmp -s - Results/$$i; \
then echo "$$i: passed"; \
- else echo "$$i: FAILED"; \
+ else echo "$$i: FAILED"; exit 2; \
fi; \
done