diff options
| author | Maxime Dénès | 2016-09-30 11:59:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-30 11:59:59 +0200 |
| commit | 367e1f913f8d0b921dc4902b83d889dac3576580 (patch) | |
| tree | 5b8ee1687a24d6cb011fbc9ce383ef8d9affec6f /lib | |
| 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 'lib')
| -rw-r--r-- | lib/flags.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index af55e9e2bb..65873e5214 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -231,7 +231,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false -let profile_ltac_cutoff = ref 0.0 +let profile_ltac_cutoff = ref 2.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode |