diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-08 12:46:09 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-08 12:46:09 +0100 |
| commit | c34744837dae427ac6cb12f5ada198862d8e1e4f (patch) | |
| tree | 66e25632e238b4b7011b95ae17903bac28669e78 /tools/CoqMakefile.in | |
| parent | c3151f4305c110757f6b7c8b448883fe29b9095c (diff) | |
| parent | 1b4bc997554894d4a317eae965f4634e04c11d20 (diff) | |
Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts
Diffstat (limited to 'tools/CoqMakefile.in')
| -rw-r--r-- | tools/CoqMakefile.in | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index de113df6a..ca02c983d 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -119,6 +119,8 @@ CAMLPKGS ?= # Option for making timing files TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -334,7 +336,7 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: print-pretty-timed:: $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' @@ -346,7 +348,7 @@ print-pretty-single-time-diff:: $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: |