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