fix

leanprover-community · Feb 27, 2025 · e14888b · e14888b
1 parent a0edece
commit e14888b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/client/src/components/editor/Editor.tsx b/client/src/components/editor/Editor.tsx
@@ -81,7 +81,7 @@ export function Editor() {
         await _leanMonaco.start(options)
 
         // JE: how do I get the editorApi or an RPC session?
-        //let infoProvider = _leanMonaco.infoProvider.editorApi
+        // let infoProvider = _leanMonaco.infoProvider.editorApi
 
         console.warn('gameId', gameId)
         await leanMonacoEditor.start(editorRef.current!, `/${worldId}/L_${levelId}.lean`, code)
@@ -106,7 +106,7 @@ export function Editor() {
         <div ref={editorRef} id="editor" />
         <div ref={infoviewRef} id="infoview" />
         {/* TODO: */}
-        <GameInfoview editorApi={null}/>
+        {/* <GameInfoview editorApi={null}/> */}
       </Split>
       {editor && typewriterMode && <Typewriter />}
     </div>