You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Call :LeanTermGoal twice, this opens a floating window and moves the cursor into it.
Open a nested popup and move the cursor into the nested popup. (requires Lean 4)
The floating window disappears and the nested popup moves to the top-left corner.
This is probably due to this change in neovim 0.6: neovim/neovim#16557 I'm not sure what the best solution is, but we might need to roll our own floating windows.
The text was updated successfully, but these errors were encountered:
:LeanTermGoal
twice, this opens a floating window and moves the cursor into it.This is probably due to this change in neovim 0.6: neovim/neovim#16557 I'm not sure what the best solution is, but we might need to roll our own floating windows.
The text was updated successfully, but these errors were encountered: