From f24d790416342aff4deb13b095cbbd9d7eddc2e6 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sat, 20 May 2017 13:47:45 +0200 Subject: [PATCH] chore(tests/lean/fail): update to current syntax --- tests/lean/fail/run_command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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"