Notice the date of my initial post :-) Nobody else complained since then, so that means it's not a critical problem. If it's not a priority, feel free to leave it alone. Another reason for changing the names of those settings is that there were only 4 of them left (however, this is not related to how many times they are used in the code, could be a much better number and in this case you are right to be worried that changes can break things). But this is certainly much better than 40 or 400 settings that need to be renamed.
-- You received this message because you are subscribed to the Google Groups "leo-editor" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/leo-editor?hl=en.
