ui.gadgets.editors: tweak caret-style and fix docs
authorJohn Benediktsson <mrjbq7@gmail.com>
Thu, 8 Sep 2022 18:37:44 +0000 (11:37 -0700)
committerJohn Benediktsson <mrjbq7@gmail.com>
Thu, 8 Sep 2022 18:37:44 +0000 (11:37 -0700)
commitc69c380ffe150b5a9115c7780fdf365283360b89
tree98460f2a35264cf8b1fae37c37b75cc8b1c4e998
parent4843bd64ead67e74c22eb715eac3ca814304250a
ui.gadgets.editors: tweak caret-style and fix docs
basis/ui/gadgets/editors/editors-docs.factor
basis/ui/gadgets/editors/editors.factor