Skip to content

Commit

Permalink
Better timer (fix build on mac)
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Jan 29, 2025
1 parent 3c0618f commit 1e17dcd
Showing 1 changed file with 13 additions and 2 deletions.
15 changes: 13 additions & 2 deletions Makefile.local.common
Original file line number Diff line number Diff line change
@@ -1,9 +1,20 @@
TIMED?=
TIMECMD?=
STDTIME?=/usr/bin/time -f "$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
# Use command time on linux, gtime on Mac OS
TIMEFMT?="$(if $(findstring undefined, $(flavor 1)),$@,$(1)) (real: %e, user: %U, sys: %S, mem: %M ko)"
ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?))
STDTIME_FULL?=command time -f $(TIMEFMT)
else
ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?))
STDTIME_FULL?=gtime -f $(TIMEFMT)
else
STDTIME_FULL?=command time
endif
endif
STDTIME?=$(STDTIME_FULL)

TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
TIMECMD_FULL?=
STDTIME_FULL?=/usr/bin/time -f "$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
TIMER_FULL=$(if $(TIMED), $(STDTIME_FULL), $(TIMECMD_FULL))

COQ_VERSION_FILE = .coq-version
Expand Down

0 comments on commit 1e17dcd

Please sign in to comment.