diff --git a/test/c/Makefile b/test/c/Makefile index 1284d98f0540c5b81381aa054d484c9cac2b3a99..3f2df78403aeed8e544f38e5481c0bbea69d4f27 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -47,12 +47,12 @@ test_gcc: done time_gcc: - @for i in $(BENCHS); do \ + @for i in $(PROGS); do \ echo -n "$$i: "; $(TIME) ./$$i.gcc; \ done time_compcert: - @for i in $(BENCHS); do \ + @for i in $(PROGS); do \ echo -n "$$i: "; $(TIME) ./$$i.compcert; \ done