diff options
Diffstat (limited to 'test/c/Makefile')
-rw-r--r-- | test/c/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/c/Makefile b/test/c/Makefile index 7b6d63c7..ed70d18e 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -30,7 +30,7 @@ all_gcc: $(PROGS:%=%.gcc) %.gcc: %.c $(CC) $(CFLAGS) -o $*.gcc $*.c $(LIBS) -test_compcert: +test: @for i in $(PROGS); do \ if ./$$i.compcert | cmp -s - Results/$$i; \ then echo "$$i: passed"; \ @@ -51,7 +51,7 @@ time_gcc: echo -n "$$i: "; $(TIME) ./$$i.gcc; \ done -time_compcert: +time: @for i in $(PROGS); do \ echo -n "$$i: "; $(TIME) ./$$i.compcert; \ done |