etc/options
changeset 65141 c706b57b1694
parent 65056 002b4c8c366e
child 65264 7e6ecd04b5fe
     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"