diff options
author | 2016-09-20 14:03:18 -0400 | |
---|---|---|
committer | 2016-09-20 14:03:18 -0400 | |
commit | f230ff18423143eb4dd4cea5b30b22f49b9ce049 (patch) | |
tree | dd6dfa7d3fc1fbeac5390ed50d4ea3fdc9c44b35 | |
parent | 8e448c450e98a99f074599f0ffe8f1b48db2df14 (diff) |
Allow passing PROFILE=1 to make for -profile-ltac
-rw-r--r-- | Makefile | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -5,6 +5,7 @@ TIMECMD?= STDTIME?=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) +PROFILE?= VERBOSE?= SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) @@ -59,9 +60,13 @@ else COQPRIME_FOLDER := coqprime ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5 else +ifneq ($(PROFILE),) +OTHERFLAGS ?= -profile-ltac -w "-deprecated-appcontext -notation-overridden" +else OTHERFLAGS ?= -w "-deprecated-appcontext -notation-overridden" endif endif +endif COQPATH?=$(shell pwd)/$(COQPRIME_FOLDER) export COQPATH |