diff options
Diffstat (limited to 'test/c')
-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 ed70d18e..9c57a3f1 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -46,12 +46,12 @@ test_gcc: fi; \ done -time_gcc: +bench_gcc: @for i in $(PROGS); do \ echo -n "$$i: "; $(TIME) ./$$i.gcc; \ done -time: +bench: @for i in $(PROGS); do \ echo -n "$$i: "; $(TIME) ./$$i.compcert; \ done |