From f42bd8f6935e75e9fc8cdfa427b7006a389ff256 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 23 Dec 2020 19:11:43 +0100 Subject: [PATCH] chore: deactivate server tests for now --- tests/lean/server/diags.lean | 3 +-- tests/lean/server/edits.lean | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) 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