From 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 29 Sep 2016 14:32:50 -0400
Subject: Set the default LtacProf cutoff to 2%

This was the original value from Tobias' code.  When a user passes
-profile-ltac on the command line, or inserts [Show Ltac Profile] in the
document, the most useful default behavior is to not overload them with
useless information.  When GUI clients want to display fancier profiling
information, there is no cost to the user to requiring them to specify
what cutoff they want.  If the GUI client does not have any special
LtacProf handling, the most useful presentation is again the one that
cuts off the display at 2% total time.
---
 lib/flags.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

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
-- 
cgit v1.2.3