On Monday, November 18, 2013 4:12:52 PM UTC+1, Terry wrote: > > > I don't know what Edward did with myLeoSettings.leo a couple of weeks > back, but you, Jerry, I think were just reporting that the menu > (non)highlighting bug returned when you compiled the stylesheet from > the outline with the script? I'll look in to that. >
Yes, that's what happened. I had to delete the whole theme, and copy it anew from leosettings.leo. However, the problem of unnecessary complexity still remains: just count how many times the same parameter may be defined in the settings. It's quite confusing, especially for those who not used to it. This, as I explained in an earlier post, may results in a lot of frustration, when you change the setting in one location, expecting to see the change appear the next time the program restarts, and that's not what happens! The straighforward way of managing the settings, in my NEWBIE opinion, would be to have each setting appear one time only. By the way, is it possible to implement the settings without having to restart Leo? -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to leo-editor+unsubscr...@googlegroups.com. To post to this group, send email to leo-editor@googlegroups.com. Visit this group at http://groups.google.com/group/leo-editor. For more options, visit https://groups.google.com/groups/opt_out.
