From 7b3c22cebb0feaf8f1d4c2bcf3057be7ef36fcfd Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Sun, 5 Oct 2025 11:38:41 +0200 Subject: [PATCH] test: disable flaky interactive diag tests (#10673) --- .../{highlightMatches.lean => highlightMatches.lean.disabled} | 0 ...ctiveDiagnostics.lean => interactiveDiagnostics.lean.disabled} | 0 .../{interactiveTraces.lean => interactiveTraces.lean.disabled} | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename tests/lean/interactive/{highlightMatches.lean => highlightMatches.lean.disabled} (100%) rename tests/lean/interactive/{interactiveDiagnostics.lean => interactiveDiagnostics.lean.disabled} (100%) rename tests/lean/interactive/{interactiveTraces.lean => interactiveTraces.lean.disabled} (100%) diff --git a/tests/lean/interactive/highlightMatches.lean b/tests/lean/interactive/highlightMatches.lean.disabled similarity index 100% rename from tests/lean/interactive/highlightMatches.lean rename to tests/lean/interactive/highlightMatches.lean.disabled diff --git a/tests/lean/interactive/interactiveDiagnostics.lean b/tests/lean/interactive/interactiveDiagnostics.lean.disabled similarity index 100% rename from tests/lean/interactive/interactiveDiagnostics.lean rename to tests/lean/interactive/interactiveDiagnostics.lean.disabled diff --git a/tests/lean/interactive/interactiveTraces.lean b/tests/lean/interactive/interactiveTraces.lean.disabled similarity index 100% rename from tests/lean/interactive/interactiveTraces.lean rename to tests/lean/interactive/interactiveTraces.lean.disabled