chore: Remove unnecessary unsafe's #29

Merged
aniva merged 1 commits from misc/cleanup into dev 2023-11-06 11:44:58 -08:00
2 changed files with 2 additions and 3 deletions

View File

@ -22,7 +22,7 @@ def parseCommand (s: String): Except String Protocol.Command := do
return { cmd := s.take offset, payload := payload }
| .none => throw "Command is empty"
unsafe def loop : MainM Unit := do
partial def loop : MainM Unit := do
let state ← get
let command ← (← IO.getStdin).getLine
if command.trim.length = 0 then return ()

View File

@ -6,8 +6,7 @@ import Test.Serial
open Pantograph.Test
unsafe def main := do
Lean.enableInitializersExecution
def main := do
Lean.initSearchPath (← Lean.findSysroot)
let suites := [