diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-10 19:54:52 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-10 19:54:52 -0400 |
| commit | aa81e1ffd569bde9012164b27b0fd01190f6aa0b (patch) | |
| tree | c8cd77eae4b2674ca64275ca9fd4fa5bca1a4da1 /Makefile | |
| parent | 9279ff69732ca873758365518de8105c250ecd23 (diff) | |
Factor out -w "-notation-overridden" in Makefile
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 2 insertions, 3 deletions
@@ -110,10 +110,9 @@ COQPRIME_FOLDER := coqprime ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5 else ifneq ($(PROFILE),) -OTHERFLAGS += -profile-ltac -w "-notation-overridden" -else -OTHERFLAGS += -w "-notation-overridden" +OTHERFLAGS += -profile-ltac endif +OTHERFLAGS += -w "-notation-overridden" endif COQPATH?=${CURDIR}/$(COQPRIME_FOLDER) |