diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-15 23:06:35 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-15 23:06:39 -0400 |
commit | a3620b2a73efff93163c0c0dfc7b7eedfbc50ef7 (patch) | |
tree | 3d63382a93882d4e536780b5c7ed2b3ed00db4a5 /Makefile | |
parent | 29ad742d76dca90ec9c8d03ab6f4359ccf053a90 (diff) |
Fix notation-overriden warning issues
This change is necessary because we've added -compat 8.6.
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 6 |
1 files changed, 2 insertions, 4 deletions
@@ -93,12 +93,10 @@ printlite:: COQPRIME_FOLDER := coqprime ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5 else -ifeq ($(OTHERFLAGS),) ifneq ($(PROFILE),) -OTHERFLAGS := -profile-ltac -w "-notation-overridden" +OTHERFLAGS += -profile-ltac -w "-notation-overridden" else -OTHERFLAGS := -w "-notation-overridden" -endif +OTHERFLAGS += -w "-notation-overridden" endif endif |