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.
Plugin default: false
Type: null or boolean or raw lua code
Default:
null
Declared by:
plugins.lean.infoview.lean3.showFilter
Plugin default: true
Type: null or boolean or raw lua code
Default:
null
Declared by: