plugins.lean.settings.stderr.enable
Redirect Lean’s stderr messages somewhere (to a buffer by default).
Type: null or boolean or raw lua code
Default:
null
Plugin default: true
Declared by:
plugins.lean.settings.stderr.height
Height of the window.
Type: null or positive integer, meaning >0, or raw lua code
Default:
null
Plugin default: 5
Declared by:
plugins.lean.settings.stderr.on_lines
A callback which will be called with (multi-line) stderr output.
Type: null or lua function string
Default:
null
Plugin default: "nil"
Declared by: