mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-03 00:55:00 +03:00
[ fix ] debugging printing
This commit is contained in:
parent
b68fa077af
commit
9f5cacf31e
@ -663,9 +663,7 @@ dumpHole' : {auto u : Ref UST UState} ->
|
||||
dumpHole' lvl hole
|
||||
= do ust <- get UST
|
||||
defs <- get Ctxt
|
||||
if keepLog lvl (logLevel $ session $ options defs)
|
||||
then pure ()
|
||||
else do
|
||||
when (keepLog lvl (logLevel $ session $ options defs)) $ do
|
||||
defs <- get Ctxt
|
||||
case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
|
||||
Nothing => pure ()
|
||||
|
Loading…
Reference in New Issue
Block a user