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 #-------------------------------------------------------------------------------