diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 11:59:59 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 11:59:59 +0200 |
| commit | 367e1f913f8d0b921dc4902b83d889dac3576580 (patch) | |
| tree | 5b8ee1687a24d6cb011fbc9ce383ef8d9affec6f /test-suite/Makefile | |
| parent | 10545881bb05aedafc512e211a4df9e7433750e7 (diff) | |
| parent | 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 (diff) | |
Merge remote-tracking branch 'github/pr/302' into v8.6
Was PR#302: Set the default LtacProf cutoff to 2%
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index acf1dae05..9d7444d7a 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -51,7 +51,7 @@ SINGLE_QUOTE=" get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1))))) # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1))) -has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) +has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command)) |