diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-11 13:38:47 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-11 13:38:47 -0400 |
| commit | 7146036f5a4555840a75b1fb564ee3c1b54623dc (patch) | |
| tree | ded017dae3c8f0fb62f173d6f9baab338773a5e4 /Makefile | |
| parent | df5218b25d73bc95becc6d1c9db124951dccd925 (diff) | |
s/appcontext/context/
They mean the same thing since 8.5, and appcontext is deprecated.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -76,9 +76,9 @@ COQPRIME_FOLDER := coqprime ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5 else ifneq ($(PROFILE),) -OTHERFLAGS ?= -profile-ltac -w "-deprecated-appcontext -notation-overridden" +OTHERFLAGS ?= -profile-ltac -w "-notation-overridden" else -OTHERFLAGS ?= -w "-deprecated-appcontext -notation-overridden" +OTHERFLAGS ?= -w "-notation-overridden" endif endif |