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

fix error formatting bug #136

Merged
merged 3 commits into from
Sep 29, 2023
Merged

fix error formatting bug #136

merged 3 commits into from
Sep 29, 2023

Conversation

icecream17
Copy link
Contributor

@icecream17 icecream17 commented Sep 29, 2023

As seen in https://github.com/metamath/set.mm/actions/runs/6345667560/job/17238038357?pr=3522 the "__" is interpreted as the markdown bold syntax, so this should be escaped

image

EDIT: This is kinda weird since there are no underscores at the end of the message...

As seen in https://github.com/metamath/set.mm/actions/runs/6345667560/job/17238038357?pr=3522
the "__" is interpreted as the markdown bold syntax, so this should be escaped
@digama0
Copy link
Member

digama0 commented Sep 29, 2023

o.O I had no idea there was markdownish formatting there. I assume it's something custom provided by the snippets library, I don't think it is actual markdown because markdown is HTML and that doesn't make too much sense in a CLI output.

@digama0
Copy link
Member

digama0 commented Sep 29, 2023

Here's the formatting logic. Apparently it just handles __ specifically, as toggling emphasis. (Maybe we should use that sometimes.)

@icecream17
Copy link
Contributor Author

icecream17 commented Sep 29, 2023

Hmm, then I'm not sure this would work. This might just display as \_\_, at least that's what the code and rust-lang/annotate-snippets-rs#53 suggests

@digama0
Copy link
Member

digama0 commented Sep 29, 2023

Does a zero-width space work?

@digama0 digama0 merged commit 81c83b8 into metamath:main Sep 29, 2023
@icecream17 icecream17 deleted the patch-1 branch September 29, 2023 12:13
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.

2 participants