aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorJason Gross2018-07-26 12:02:59 -0400
committerJason Gross2018-08-24 12:30:04 -0400
commit522fbcc49a44aa5cbae6b0c13dc35f53f48227a4 (patch)
tree00e6770398e634f3198c6f3faf180fa6832baada /tools
parent05d13bf516a75da38bacbb62608528f8dceb34fd (diff)
Fix ordering of before/after in print-pretty-timed-*
Fixes #8158
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in8
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 8b6822a4ed..403ad61798 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -343,19 +343,19 @@ 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) --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)
+ $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_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'
+ @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
$(HIDE)false
else
ifeq (,$(AFTER))
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'
+ @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
$(HIDE)false
else
print-pretty-single-time-diff::
- $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
endif
endif
pretty-timed: