diff --git a/tests/lean/fail/run_command.lean b/tests/lean/fail/run_command.lean index 17a3b3c358..1a0b01c768 100644 --- a/tests/lean/fail/run_command.lean +++ b/tests/lean/fail/run_command.lean @@ -1 +1 @@ -run_command tactic.fail "Error" +run_cmd tactic.fail "Error"