max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: raise default profiler.threshold to 100ms

Browse source
This commit is contained in:
Sebastian Ullrich 2021-07-28 13:35:23 +02:00
parent 88492e38a7
commit 2e8075b015
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/profiling.cpp
View file

@ -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 {