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.

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

Add Coq support #514

Merged
merged 3 commits into from
Oct 20, 2021
Merged

Add Coq support #514

merged 3 commits into from
Oct 20, 2021

Conversation

exoego
Copy link
Contributor

@exoego exoego commented Oct 20, 2021

Addresses #490

Original image is https://github.com/coq/coq/blob/master/ide/coqide/coq.png

Preview

True color Safe color
image image

@spenserblack
Copy link
Collaborator

Thank you!
There will likely be a merge conflict with #513. Just something to look out for.

@exoego
Copy link
Contributor Author

exoego commented Oct 20, 2021

I will update after #513 get merged

# Conflicts:
#	src/info/langs/language.rs
@o2sh o2sh self-requested a review October 20, 2021 14:43
Copy link
Owner

@o2sh o2sh left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's a very nice ascii art @exoego,
I left a suggestion regarding the use of bright colors.
Aside from that, everything LGTM 👍

src/info/langs/language.rs Outdated Show resolved Hide resolved
Copy link
Collaborator

@spenserblack spenserblack left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the PR!
I had a concern about the color choices.

src/info/langs/language.rs Outdated Show resolved Hide resolved
@spenserblack
Copy link
Collaborator

Oh, lol, I see @o2sh had the exact same recommendation 😆

@exoego
Copy link
Contributor Author

exoego commented Oct 20, 2021

Changed BrightYellow to White

@o2sh o2sh merged commit 5074a16 into o2sh:main Oct 20, 2021
@exoego exoego deleted the add-coq branch October 20, 2021 15:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants