From 3dfd14dfffaaa7e5479e2c40c10ff94848681d93 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 31 Jan 2022 16:45:57 -0800
Subject: [PATCH] chore: fix test

---
 tests/{ => lean}/361.lean        |  0
 tests/lean/361.lean.expected.out | 19 ++++++++++++++++++-
 2 files changed, 18 insertions(+), 1 deletion(-)
 rename tests/{ => lean}/361.lean (100%)

diff --git a/tests/361.lean b/tests/lean/361.lean
similarity index 100%
rename from tests/361.lean
rename to tests/lean/361.lean
diff --git a/tests/lean/361.lean.expected.out b/tests/lean/361.lean.expected.out
index 59ab0eb12c..18ab15f98c 100644
--- a/tests/lean/361.lean.expected.out
+++ b/tests/lean/361.lean.expected.out
@@ -1 +1,18 @@
-file '361.lean' not found
+361.lean:3:0: error: expected '{' or tactic
+361.lean:1:60-1:62: error: unsolved goals
+p q r : Prop
+h1 : p ∨ q
+h2 : p → q
+⊢ q
+361.lean:6:0: error: unexpected end of input; expected '{'
+361.lean:5:11-5:13: error: unsolved goals
+p q r : Prop
+h2 : p → q
+h✝ : p
+⊢ q
+361.lean:3:60-5:13: error: unsolved goals
+case inr
+p q r : Prop
+h2 : p → q
+h✝ : q
+⊢ q