etc/options

--- a/etc/options	Fri Nov 01 14:10:52 2024 +0000
+++ b/etc/options	Fri Nov 01 16:57:33 2024 +0100
@@ -309,6 +309,9 @@
 public option editor_output_state : bool = false
   -- "implicit output of proof state"
 
+public option editor_auto_hovering : bool = true
+  -- "automatic mouse hovering without keyboard modifier"
+
 public option editor_document_session : string = ""
   -- "session for interactive document preparation"