clarified modules;
authorwenzelm
Tue Mar 07 15:35:54 2017 +0100 (2017-03-07)
changeset 65141c706b57b1694
parent 65140 1191df79aa1c
child 65142 368004bed323
clarified modules;
etc/options
src/Tools/jEdit/etc/options
     1.1 --- a/etc/options	Tue Mar 07 14:51:52 2017 +0100
     1.2 +++ b/etc/options	Tue Mar 07 15:35:54 2017 +0100
     1.3 @@ -193,6 +193,18 @@
     1.4    -- "limit for completion within the formal context"
     1.5  
     1.6  
     1.7 +section "Spell Checker"
     1.8 +
     1.9 +public option spell_checker : bool = true
    1.10 +  -- "enable spell-checker for prose words within document text, comments etc."
    1.11 +
    1.12 +public option spell_checker_dictionary : string = "en"
    1.13 +  -- "spell-checker dictionary name"
    1.14 +
    1.15 +public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
    1.16 +  -- "relevant markup elements for spell-checker, separated by commas"
    1.17 +
    1.18 +
    1.19  section "Secure Shell"
    1.20  
    1.21  option ssh_config_dir : string = "~/.ssh"
     2.1 --- a/src/Tools/jEdit/etc/options	Tue Mar 07 14:51:52 2017 +0100
     2.2 +++ b/src/Tools/jEdit/etc/options	Tue Mar 07 15:35:54 2017 +0100
     2.3 @@ -73,18 +73,6 @@
     2.4    -- "glob patterns to ignore in file-system path completion (separated by colons)"
     2.5  
     2.6  
     2.7 -section "Spell Checker"
     2.8 -
     2.9 -public option spell_checker : bool = true
    2.10 -  -- "enable spell-checker for prose words within document text, comments etc."
    2.11 -
    2.12 -public option spell_checker_dictionary : string = "en"
    2.13 -  -- "spell-checker dictionary name"
    2.14 -
    2.15 -public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
    2.16 -  -- "relevant markup elements for spell-checker, separated by commas"
    2.17 -
    2.18 -
    2.19  section "Rendering of Document Content"
    2.20  
    2.21  option outdated_color : string = "EEE3E3FF"