aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 92de63668..8a3f2cac4 100644
--- a/Makefile
+++ b/Makefile
@@ -545,8 +545,9 @@ $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%.hs) : %.hs : %.v
$(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp
$(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp | sed -f src/Experiments/NewPipeline/haskell.sed > $@ && rm -f $@.tmp
+# pass -w -20 to disable the unused argument warning
$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) : % : %.ml
- $(TIMER_FULL) ocamlopt -o $@ $<
+ $(TIMER_FULL) ocamlopt -w -20 -o $@ $<
$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) : % : %.hs
$(TIMER_FULL) $(GHC) $(GHCFLAGS) -o $@ $<