diff options
Diffstat (limited to 'test/c/Makefile')
| -rw-r--r-- | test/c/Makefile | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test/c/Makefile b/test/c/Makefile index 16fead48..88969342 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -50,6 +50,11 @@ time_gcc: echo -n "$$i: "; $(TIME) ./$$i.gcc; \ done +time_compcert: + @for i in $(PROGS); do \ + echo -n "$$i: "; $(TIME) ./$$i.compcert; \ + done + clean: rm -f *.compcert *.gcc rm -f *.light.c *.s *.o *~ |