bug where commandline would be hidden

leanprover-community · Aug 30, 2023 · 714634f · 714634f
1 parent d7fdd95
commit 714634f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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>
 }