From fbdc1afe34ffa6e38a13c0383a0a719785d32f56 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 30 Jan 2023 13:18:02 +0100
Subject: [PATCH] hide command line properly

---
 client/src/components/infoview/goals.tsx | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index d394d8a..0ee317f 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -159,9 +159,7 @@ export const Goal = React.memo((props: GoalProps) => {
         { assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        <div className={commandLineMode ? "" : "hidden"}>
-            <CommandLine />
-        </div>
+        {commandLineMode && <CommandLine />}
         {!filter.reverse && goalLi}
         {showHints && hints}
     </div>