etc/options
changeset 65141 c706b57b1694
parent 65056 002b4c8c366e
child 65264 7e6ecd04b5fe
equal deleted inserted replaced
65140:1191df79aa1c 65141:c706b57b1694
   191 
   191 
   192 public option completion_limit : int = 40
   192 public option completion_limit : int = 40
   193   -- "limit for completion within the formal context"
   193   -- "limit for completion within the formal context"
   194 
   194 
   195 
   195 
       
   196 section "Spell Checker"
       
   197 
       
   198 public option spell_checker : bool = true
       
   199   -- "enable spell-checker for prose words within document text, comments etc."
       
   200 
       
   201 public option spell_checker_dictionary : string = "en"
       
   202   -- "spell-checker dictionary name"
       
   203 
       
   204 public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
       
   205   -- "relevant markup elements for spell-checker, separated by commas"
       
   206 
       
   207 
   196 section "Secure Shell"
   208 section "Secure Shell"
   197 
   209 
   198 option ssh_config_dir : string = "~/.ssh"
   210 option ssh_config_dir : string = "~/.ssh"
   199   -- "SSH configuration directory"
   211   -- "SSH configuration directory"
   200 
   212