aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-07-24 19:23:24 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-07-24 19:24:05 -0400
commitee334b4bff8450afbc580a410fe1225b51260e05 (patch)
tree89bd6c5549e8adfdd81bda0ddc8bedec66a33273 /Makefile
parent8772868f6b3796d6dd83a76ba2d0525388a71117 (diff)
User TIMER_FULL for .ml, .hs, compiled files
This gives them different entries in the timing diff
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 4 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 2dc80f34c..d239e2d3e 100644
--- a/Makefile
+++ b/Makefile
@@ -484,19 +484,19 @@ STANDALONE := \
$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%.ml) : %.ml : %.v src/Experiments/NewPipeline/StandaloneOCamlMain.vo
$(SHOW)'COQC $< > $@'
- $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp
+ $(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp
$(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp > $@ && rm -f $@.tmp
$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%.hs) : %.hs : %.v src/Experiments/NewPipeline/StandaloneHaskellMain.vo src/Experiments/NewPipeline/haskell.sed
$(SHOW)'COQC $< > $@'
- $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp
+ $(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
$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) : % : %.ml
- $(TIMER) ocamlopt -o $@ $<
+ $(TIMER_FULL) ocamlopt -o $@ $<
$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) : % : %.hs
- $(TIMER) $(GHC) $(GHCFLAGS) -o $@ $<
+ $(TIMER_FULL) $(GHC) $(GHCFLAGS) -o $@ $<
standalone: standalone-haskell standalone-ocaml