RessourceEditor.py
changeset 579 bc333e073aa3
parent 578 73138d14d88d
child 586 9aa96a36cf33
equal deleted inserted replaced
578:73138d14d88d 579:bc333e073aa3
    70         pass
    70         pass
    71 
    71 
    72     def RefreshScaling(self, refresh=True):
    72     def RefreshScaling(self, refresh=True):
    73         pass
    73         pass
    74 
    74 
    75     def ClearHighlights(self):
    75     def ClearHighlights(self, highlight_type=None):
    76         pass
    76         pass
    77 
    77 
    78 #-------------------------------------------------------------------------------
    78 #-------------------------------------------------------------------------------
    79 #                            Resource Editor class
    79 #                            Resource Editor class
    80 #-------------------------------------------------------------------------------
    80 #-------------------------------------------------------------------------------