feat(ui-ext): make 'mousehide' into proper ui_option (#25532)

This commit is contained in:
Jaehoon Hwang
2023-10-09 01:48:24 -07:00
committed by GitHub
parent f96f8566b5
commit dacd34364f
4 changed files with 11 additions and 0 deletions

View File

@@ -5452,9 +5452,11 @@ return {
]=],
enable_if = false,
full_name = 'mousehide',
redraw = { 'ui_option' },
scope = { 'global' },
short_desc = N_('hide mouse pointer while typing'),
type = 'bool',
varname = 'p_mh',
},
{
abbreviation = 'mousem',