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: