From 2e8075b015a643dc2ec36aba543d46d93f077019 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 28 Jul 2021 13:35:23 +0200 Subject: [PATCH] chore: raise default `profiler.threshold` to 100ms --- src/library/profiling.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/profiling.cpp b/src/library/profiling.cpp index 0ceae478c3..46dcb55af0 100644 --- a/src/library/profiling.cpp +++ b/src/library/profiling.cpp @@ -12,7 +12,7 @@ Author: Gabriel Ebner #endif #ifndef LEAN_DEFAULT_PROFILER_THRESHOLD -#define LEAN_DEFAULT_PROFILER_THRESHOLD 0 +#define LEAN_DEFAULT_PROFILER_THRESHOLD 100 #endif namespace lean {