max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: deactivate server tests for now

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-23 19:11:43 +01:00
parent 2740a8c012
commit f42bd8f693
2 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/server/diags.lean
View file

@ -1,3 +1,2 @@
#lang lean4
import Lean.Server
#eval Lean.Server.Test.runWithInputFile "./diags_client.log" none -- The builtin search path seems to be fine
--#eval Lean.Server.Test.runWithInputFile "./diags_client.log" none -- The builtin search path seems to be fine

3
tests/lean/server/edits.lean
View file

@ -1,3 +1,2 @@
#lang lean4
import Lean.Server
#eval Lean.Server.Test.runWithInputFile "./edits_client.log" none -- The builtin search path seems to be fine
--#eval Lean.Server.Test.runWithInputFile "./edits_client.log" none -- The builtin search path seems to be fine