The new code completes the following issues: - #993: Use '-', not underscore for settings names <https://github.com/leo-editor/leo-editor/issues/993>
The script `regularize settings names` did the work. A copy of this script is now in scripts.leo (leo-scripts-leo opens this file). - #902: Many unused/missing settings <https://github.com/leo-editor/leo-editor/issues/902> `@button check-settings` does the checking. This script checks for missing and unused settings. A copy is now in scripts.leo. This script contains many unavoidable special cases, which are cleanly encapsulated in two filter functions. This script does not check settings used in style sheets. Figuring out which style sheets are in effect would be difficult, and not useful in any case. *Summary* Many changes were made to Leo and its settings. Please reopen #902 if there are problems. Many unused settings have been retired. See #902 for a full list, along with other details. At present, the retired settings still exist in leoSettings.leo. They have no effect because they exist outside the @settings tree. The @button check-settings script in leoSettings.leo now passes, proving that unused or missing settings are mostly behind us. I'll run this button before each new release. However, settings related to style sheets are not checked. This work took at least two full working days. Imo, it was worth the effort. 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 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.
