diff -r 1191df79aa1c -r c706b57b1694 etc/options --- a/etc/options Tue Mar 07 14:51:52 2017 +0100 +++ b/etc/options Tue Mar 07 15:35:54 2017 +0100 @@ -193,6 +193,18 @@ -- "limit for completion within the formal context" +section "Spell Checker" + +public option spell_checker : bool = true + -- "enable spell-checker for prose words within document text, comments etc." + +public option spell_checker_dictionary : string = "en" + -- "spell-checker dictionary name" + +public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment" + -- "relevant markup elements for spell-checker, separated by commas" + + section "Secure Shell" option ssh_config_dir : string = "~/.ssh"