diff --git a/GNUmakefile b/GNUmakefile index 723f438319..3de8a05bf9 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -1,4 +1,4 @@ -AGDA_EXEC?=agda -W error +AGDA_EXEC?=agda -W error -W noNoEquivWhenSplitting FIX_WHITESPACE?=fix-whitespace RTS_OPTIONS=+RTS -H3G -RTS AGDA=$(AGDA_EXEC) $(RTS_OPTIONS)