plugins.lean.infoview.lean3.mouseEvents
Setting this to true will simulate mouse events in the Lean 3 infoview, this is buggy
at the moment so you can use the I/i keybindings to manually trigger these.
Type: null or boolean or raw lua code
Default:
null
Plugin default: false
Declared by:
plugins.lean.infoview.lean3.showFilter
Type: null or boolean or raw lua code
Default:
null
Plugin default: true
Declared by: