phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

reintroduce infoProvider.dispose();

Browse Source 
We need to find another solution to avoid the unsubscribe error
This commit is contained in:
Alexander Bentkamp
2023-01-25 11:30:26 +01:00
parent 6c9ba14fd2
commit 3d349f9a6b
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/Level.tsx
+1 -1
View File
@@ -280,7 +280,7 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo
setInfoProvider(infoProvider) setInfoProvider(infoProvider)
setInfoviewApi(infoviewApi) setInfoviewApi(infoviewApi)
return () => { editor.setModel(null); editor.dispose() } return () => { editor.setModel(null); infoProvider.dispose(); editor.dispose() }
}, []) }, [])
const {leanClient, leanClientStarted} = useLeanClient() const {leanClient, leanClientStarted} = useLeanClient()