From a07e9df66e16609e8bdc1dffba317dfdae412152 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 7 Jun 2022 17:42:09 +0200
Subject: [PATCH] fix: use goal prefix in plain goal response

---
 src/Lean/Widget/InteractiveGoal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 5e1ad26e8b..6e47d35d68 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -50,7 +50,7 @@ def pretty (g : InteractiveGoal) : Format := Id.run do
       | none =>
         ret := ret ++ Format.group f!"{names} :{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
   ret := addLine ret
-  ret ++ f!"⊢ {Format.nest indent g.type.stripTags}"
+  ret ++ f!"{g.goalPrefix}{Format.nest indent g.type.stripTags}"
 
 end InteractiveGoal