lean4-htt/tests/lean/server/edits.lean
2020-12-23 20:00:36 +01:00

2 lines
131 B
Text

import Lean.Server
--#eval Lean.Server.Test.runWithInputFile "./edits_client.log" none -- The builtin search path seems to be fine