aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-09-20 14:03:18 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-09-20 14:03:18 -0400
commitf230ff18423143eb4dd4cea5b30b22f49b9ce049 (patch)
treedd6dfa7d3fc1fbeac5390ed50d4ea3fdc9c44b35 /Makefile
parent8e448c450e98a99f074599f0ffe8f1b48db2df14 (diff)
Allow passing PROFILE=1 to make for -profile-ltac
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 5 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 0deb7bd28..6a643fa7b 100644
--- a/Makefile
+++ b/Makefile
@@ -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