Update placeholders when env changes

This commit is contained in:
Gregory Schier
2023-10-28 19:14:51 -07:00
parent 613081728d
commit 77e5142a7c
@@ -9,7 +9,7 @@ class PlaceholderWidget extends WidgetType {
super(); super();
} }
eq(other: PlaceholderWidget) { eq(other: PlaceholderWidget) {
return this.name == other.name; return this.name == other.name && this.isExistingVariable == other.isExistingVariable;
} }
toDOM() { toDOM() {
const elt = document.createElement('span'); const elt = document.createElement('span');