controls/VariablePanel.py
branchpython3
changeset 3765 88fe6fc9fd38
parent 3764 d92c1a3dafa7
child 3789 8def429216ca
--- a/controls/VariablePanel.py	Fri Oct 28 18:59:04 2022 +0800
+++ b/controls/VariablePanel.py	Fri Oct 28 19:39:17 2022 +0800
@@ -685,9 +685,6 @@
             else:
                 self.VariablesGrid.SetColSize(col, self.ColSettings["size"][col])
 
-    def __del__(self):
-        self.RefreshHighlightsTimer.Stop()
-
     def SetTagName(self, tagname):
         self.TagName = tagname
         self.BodyType = self.Controler.GetEditedElementBodyType(self.TagName)