mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 10:18:23 +03:00
[ debug ] remove max
from log
Users should be allowed to de-escalate the level of detail they're getting.
This commit is contained in:
parent
5de647cc3f
commit
0a685f8d2c
@ -116,7 +116,7 @@ defaultLogLevel = singleton [] 0
|
||||
|
||||
export
|
||||
insertLogLevel : LogLevel -> LogLevels -> LogLevels
|
||||
insertLogLevel (MkLogLevel ps n) = insertWith ps (maybe n (max n))
|
||||
insertLogLevel (MkLogLevel ps n) = insert ps n
|
||||
|
||||
----------------------------------------------------------------------------------
|
||||
-- CHECKING WHETHER TO LOG
|
||||
|
Loading…
Reference in New Issue
Block a user