diff --git a/tests/lean/server/diags.lean b/tests/lean/server/diags.lean index 4b96c6191c..a1168bb1f1 100644 --- a/tests/lean/server/diags.lean +++ b/tests/lean/server/diags.lean @@ -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 diff --git a/tests/lean/server/edits.lean b/tests/lean/server/edits.lean index cf907f4912..4295559689 100644 --- a/tests/lean/server/edits.lean +++ b/tests/lean/server/edits.lean @@ -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