chore: Remove unnecessary unsafe's
This commit is contained in:
parent
1638c308a9
commit
8182da436d
|
@ -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 ()
|
||||
|
|
|
@ -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 := [
|
||||
|
|
Loading…
Reference in New Issue