plugins.lean.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.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.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.
Type: null or lua function string
Default:
null
Plugin default: "nil"
Declared by: