From 348037abbf8cec2efb28d3e01dff0689fada1c49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 Apr 2022 15:46:28 -0700 Subject: [PATCH] chore: move `states35` to bench directory @Kha It breaks in the CI in debug mode (stack overflow). I think we have a mechanism for skipping some tests in debug mode, but I forgot how it works. --- tests/{lean/run => bench}/states35.lean | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename tests/{lean/run => bench}/states35.lean (100%) diff --git a/tests/lean/run/states35.lean b/tests/bench/states35.lean similarity index 100% rename from tests/lean/run/states35.lean rename to tests/bench/states35.lean