I found the setting in the main leoSettings.leo (config folder). However, it makes me wonder about a bigger question.
I will of course want to add that new setting to myLeoSettings.leo, but since that file was created from a much older Leo version, what other settings might be missing that I might want or need? What's a good strategy to refresh the myLeoSettings.leo file with a current base while keeping my custom settings? Rob............. On Friday, April 8, 2016 at 10:13:41 AM UTC-4, Terry Brown wrote: > > On Fri, 8 Apr 2016 08:36:46 -0500 > "Edward K. Ream" <[email protected] <javascript:>> wrote: > > > On Fri, Apr 8, 2016 at 7:57 AM, john lunzer <[email protected] > <javascript:>> wrote: > > > > > Really? How do I activate this? > > > > @bool check_for_changed_external_files = True > > > > Perhaps this should be on by default. I kinda think so. > > > > There are other settings that apply. Search for c.config in > > leoExternalFiles.py. > > > > Edward > > Ha, I didn't know about that. > > - It seems to work, apart from the text in the popup > - I can't find the code, because I can't find a reference to the > setting > - The text in the popup says "Overwrite foo.py", it should probably > say "Re-read foo.py", which is what it does when you say yes. > Although the overwrite part is correct if you say No to re-read, > then modify, then save. At that point the changed file is > overwritten. I'd probably change the text to say re-read, and if > the file's not re-read, give the user one more chance to not > overwrite the file on save - by simply not updating Leo's record > of the file's timestamp. > > Why can't I find the setting? I tried > > check_for_changed_external_files > check-for-changed-external-files > checkforcha > r:config.*external > > Maybe it's just too early in the morning. > > Cheers -Terry > -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/leo-editor. For more options, visit https://groups.google.com/d/optout.
