plugins.lean.stderr.enable
Redirect Lean’s stderr messages somewhere (to a buffer by default).
Plugin default: true
Type: null or boolean or raw lua code
Default:
null
Declared by:
plugins.lean.stderr.height
Height of the window.
Plugin default: 5
Type: null or positive integer, meaning >0, or raw lua code
Default:
null
Declared by:
plugins.lean.stderr.onLines
A callback which will be called with (multi-line) stderr output.
e.g., use:
onLines = "function(lines) vim.notify(lines) end";
if you want to redirect stderr to vim.notify
.
The default implementation will redirect to a dedicated stderr
window.
Plugin default: nil
Type: null or lua function string
Default:
null
Declared by: