diff options
| author | Maxime Dénès | 2017-07-19 17:37:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-19 17:37:48 +0200 |
| commit | d074e889b3cdfe8c292d3c52a4ed005789384fc0 (patch) | |
| tree | 1a32b01f4daa0b8473b8f8733fb9775a1fb14c09 /Makefile.common | |
| parent | 9ccba83b916523107d6c692b3147d0d91ec03411 (diff) | |
| parent | 18dd13f3717295ef3c2edce1451b0b9ac99dc5d7 (diff) | |
Merge PR #745: Add timing scripts
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/Makefile.common b/Makefile.common index 100698321a..85ecb1a08d 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,7 +12,7 @@ # Executables ########################################################################### -COQMKTOP:=bin/coqmktop$(EXE) +COQMKTOP:=bin/coqmktop$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPEXE:=bin/coqtop$(EXE) @@ -25,9 +25,15 @@ COQWC:=bin/coqwc$(EXE) COQDOC:=bin/coqdoc$(EXE) COQC:=bin/coqc$(EXE) COQWORKMGR:=bin/coqworkmgr$(EXE) +COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py +COQTIME_FILE_MAKER:=tools/TimeFileMaker.py +COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py +COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ $(COQWORKMGR) +TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ + $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) COQDEPBOOT:=bin/coqdep_boot$(EXE) OCAMLLIBDEP:=bin/ocamllibdep$(EXE) @@ -64,7 +70,7 @@ DYNLIB:=.cma endif INSTALLBIN:=install -INSTALLLIB:=install -m 644 +INSTALLLIB:=install -m 644 INSTALLSH:=./install.sh MKDIR:=install -d @@ -191,7 +197,7 @@ LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \ $(call vo_to_obj,$(ALLVO)) \ $(VFILES) $(GLOBFILES) -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: |