WIP: Expand the developer documentation #27

Draft
gremond wants to merge 294 commits from develop into developer_docs
Showing only changes of commit 66e6ddfe31 - Show all commits

View file

@ -632,7 +632,7 @@ class UserData:
default = option.value.default()
if option.isleader():
default = default[0]
value = _('{0} (the search key is "{1}")').format(value, default)
value = _('{0} (the key being sought is "{1}")').format(value, default)
option_without_index.information.set(
key,
value,