RessourceEditor.py
changeset 579 bc333e073aa3
parent 578 73138d14d88d
child 586 9aa96a36cf33
--- a/RessourceEditor.py	Tue Oct 18 22:20:10 2011 +0200
+++ b/RessourceEditor.py	Thu Oct 20 00:05:38 2011 +0200
@@ -72,7 +72,7 @@
     def RefreshScaling(self, refresh=True):
         pass
 
-    def ClearHighlights(self):
+    def ClearHighlights(self, highlight_type=None):
         pass
 
 #-------------------------------------------------------------------------------