# HG changeset patch
# User laurent
# Date 1319061938 -7200
# Node ID bc333e073aa3872d85edefb8943a81a249b88784
# Parent  73138d14d88d70c844658f613fa6f644292d2ff9
Fix bug with highlighting in ConfigurationEditor

diff -r 73138d14d88d -r bc333e073aa3 RessourceEditor.py
--- 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
 
 #-------------------------------------------------------------------------------