From aea318b48dd7e15df16eca12ba59c677671869aa Mon Sep 17 00:00:00 2001
From: Nate Sesti <sestinj@gmail.com>
Date: Fri, 2 Jun 2023 13:44:33 -0400
Subject: policy + starcoder description fixes

---
 extension/react-app/src/tabs/gui.tsx | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'extension/react-app')

diff --git a/extension/react-app/src/tabs/gui.tsx b/extension/react-app/src/tabs/gui.tsx
index 5ddddbfc..42ad4ed5 100644
--- a/extension/react-app/src/tabs/gui.tsx
+++ b/extension/react-app/src/tabs/gui.tsx
@@ -19,6 +19,7 @@ import useContinueGUIProtocol from "../hooks/useWebsocket";
 let TopGUIDiv = styled.div`
   display: grid;
   grid-template-columns: 1fr;
+  overflow: scroll;
 `;
 
 let UserInputQueueItem = styled.div`
@@ -37,7 +38,7 @@ function GUI(props: GUIProps) {
   const [waitingForSteps, setWaitingForSteps] = useState(false);
   const [userInputQueue, setUserInputQueue] = useState<string[]>([]);
   const [history, setHistory] = useState<History | undefined>();
-  //   {
+  // {
   //   timeline: [
   //     {
   //       step: {
@@ -153,8 +154,7 @@ function GUI(props: GUIProps) {
   //     },
   //   ],
   //   current_index: 0,
-  // } as any
-  // );
+  // } as any);
 
   const client = useContinueGUIProtocol();
 
@@ -211,7 +211,9 @@ function GUI(props: GUIProps) {
       {typeof client === "undefined" && (
         <>
           <Loader></Loader>
-          <p>Server disconnected</p>
+          <p style={{ textAlign: "center" }}>
+            Trying to reconnect with server...
+          </p>
         </>
       )}
       {history?.timeline.map((node: HistoryNode, index: number) => {
-- 
cgit v1.2.3-70-g09d2