From fbfec02015283ada1191c6afda5acb128f9129ab Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 22 May 2017 17:51:10 +0200 Subject: [PATCH] fix(tests): move test away from run --- tests/lean/{run => }/eqn_compiler_ctor.lean | 0 tests/lean/eqn_compiler_ctor.lean.expected.out | 1 + 2 files changed, 1 insertion(+) rename tests/lean/{run => }/eqn_compiler_ctor.lean (100%) create mode 100644 tests/lean/eqn_compiler_ctor.lean.expected.out diff --git a/tests/lean/run/eqn_compiler_ctor.lean b/tests/lean/eqn_compiler_ctor.lean similarity index 100% rename from tests/lean/run/eqn_compiler_ctor.lean rename to tests/lean/eqn_compiler_ctor.lean diff --git a/tests/lean/eqn_compiler_ctor.lean.expected.out b/tests/lean/eqn_compiler_ctor.lean.expected.out new file mode 100644 index 0000000000..6505de416b --- /dev/null +++ b/tests/lean/eqn_compiler_ctor.lean.expected.out @@ -0,0 +1 @@ +eqn_compiler_ctor.lean:10:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)