#1240 <https://github.com/leo-editor/leo-editor/issues/1240>suggests raising an alert when an external editor changes a .leo file that Leo has opened.
If the user agrees to reloading the .leo file, Leo completely restarts itself. Imo, this is the simplest thing that could possibly work. I'll consider alternatives only if there is a real need. Please report any problems. I'll merge ekr-change into devel the Friday, December 11. Edward -- 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 view this discussion on the web visit https://groups.google.com/d/msgid/leo-editor/c56d6527-504f-4314-871e-8a91a6618018n%40googlegroups.com.
