From dacd34364ff3af98bc2d357c43e3ce06638e2ce9 Mon Sep 17 00:00:00 2001
From: Jaehoon Hwang <jaehoonhwang@users.noreply.github.com>
Date: Mon, 9 Oct 2023 01:48:24 -0700
Subject: feat(ui-ext): make 'mousehide' into proper ui_option (#25532)

---
 runtime/doc/ui.txt | 1 +
 1 file changed, 1 insertion(+)

(limited to 'runtime')

diff --git a/runtime/doc/ui.txt b/runtime/doc/ui.txt
index 8784a395f2..9cf0e59854 100644
--- a/runtime/doc/ui.txt
+++ b/runtime/doc/ui.txt
@@ -211,6 +211,7 @@ the editor.
 	- 'guifontwide'
 	- 'linespace'
 	- 'mousefocus'
+	- 'mousehide'
 	- 'mousemoveevent'
 	- 'pumblend'
 	- 'showtabline'
-- 
cgit