fix: persist GoalInfoDisplay state

leanprover · Oct 17, 2024 · 480d1eb · 480d1eb
1 parent 276850a
commit 480d1eb
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
@@ -219,7 +219,6 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                 </div>
             )}
             <GoalInfoDisplay
-                key={DocumentPosition.toString(pos)}
                 pos={pos}
                 goals={goals}
                 termGoal={termGoal}