Closed Vtec234 closed 1 month ago
As seen in the recording, opening the filters tooltip collapses the tactic state.
https://github.com/user-attachments/assets/ac35b200-8692-44b1-8928-b91790b763fc
Expected behavior: Opening the tooltip does not (un)collapse the tactic state.
Actual behavior: As above.
vscode-lean4 v0.0.174
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.
Description
As seen in the recording, opening the filters tooltip collapses the tactic state.
https://github.com/user-attachments/assets/ac35b200-8692-44b1-8928-b91790b763fc
Expected behavior: Opening the tooltip does not (un)collapse the tactic state.
Actual behavior: As above.
Versions
vscode-lean4 v0.0.174Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.