From 714634fe5af7a79b58a65ffa480f38dc2dc09dc8 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Wed, 30 Aug 2023 17:31:49 +0200
Subject: [PATCH] bug where commandline would be hidden

---
 client/src/components/infoview/main.tsx | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 1160f872..5901665e 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -477,6 +477,6 @@ export function CommandLineInterface(props: { world: string, level: number, data
         </>
       : <CircularProgress />}
     </div>
-    <CommandLine proofPanelRef={proofPanelRef} hidden={proof[proof.length - 1]?.goals.length == 0}/>
+    <CommandLine proofPanelRef={proofPanelRef} hidden={!withErr && proof[proof.length - 1]?.goals.length == 0}/>
   </div>
 }