From e76dac2f7f5f9ad8c2ae64ffb07dc4f783fa37b3 Mon Sep 17 00:00:00 2001 From: James Sully Date: Thu, 1 Aug 2024 22:18:57 +1000 Subject: [PATCH] remove dedicated prio from runCmdSimple child process waiter task --- src/Sand/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Sand/Basic.lean b/src/Sand/Basic.lean index acb9acb..86405be 100644 --- a/src/Sand/Basic.lean +++ b/src/Sand/Basic.lean @@ -63,7 +63,7 @@ def runCmdSimple (cmd : String) (args : Array String := #[]) : IO Unit := do stdout := .null, stderr := .null, } - _ ← (child.wait).asTask .dedicated + _ ← (child.wait).asTask def notify (message : String) : IO Unit := do -- TODO wrap libnotify with FFI so we can do this properly