Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Search gives output in one long line (difficult to read) #282

Closed
orilahav opened this issue Feb 5, 2023 · 3 comments · Fixed by #272
Closed

Search gives output in one long line (difficult to read) #282

orilahav opened this issue Feb 5, 2023 · 3 comments · Fixed by #272
Labels
kind: bug Something isn't working part: goals and info panel
Milestone
0.1.5

Comments

@orilahav
Copy link

orilahav commented Feb 5, 2023

Here is a screenshot:

Screen Shot 2023-02-05 at 16 33 10
@Alizter
Copy link
Collaborator

Alizter commented Feb 5, 2023

This was fixed in main. Here is how it looks:
image

@Alizter Alizter closed this as completed Feb 5, 2023
@ejgallego ejgallego added this to the 0.1.5 milestone Feb 5, 2023
@ejgallego
Copy link
Owner

Indeed sorry @orilahav , this is a bug in in 0.1.4, we will release a fixed version ASAP; also our UI for Search is far from even usable, I hope we can improve it soon.

@ejgallego
Copy link
Owner

ejgallego commented Feb 6, 2023 •
edited
Loading

Note this was fixed by #272

@ejgallego ejgallego linked a pull request Feb 6, 2023 that will close this issue
[info] Fix messages panel rendering after port to react. #272
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug Something isn't working part: goals and info panel
Projects
None yet
Milestone
0.1.5
Development

Successfully merging a pull request may close this issue.

[info] Fix messages panel rendering after port to react. ejgallego/coq-lsp
3 participants
@ejgallego @Alizter @orilahav