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

Identifier labels (?id:, id:) should be <span>ned. #879

Closed
dbuenzli opened this issue Jun 18, 2022 · 1 comment · Fixed by #990
Closed

Identifier labels (?id:, id:) should be <span>ned. #879

dbuenzli opened this issue Jun 18, 2022 · 1 comment · Fixed by #990
Labels

Comments

@dbuenzli
Copy link
Contributor

dbuenzli commented Jun 18, 2022

So that we can colorize them like most syntax highlighters do.

I thought about doing a PR myself but nothing evident showed up in a quick glance. Do the labels show up as structured information or you need to munge the type identifiers ?

@dbuenzli dbuenzli added output enhancement New feature or request labels Jun 18, 2022
@dbuenzli dbuenzli changed the title Identifier labels (?id, id) should be <span>ned. Identifier labels (?id, ~id) should be <span>ned. Jun 18, 2022
@dbuenzli dbuenzli changed the title Identifier labels (?id, ~id) should be <span>ned. Identifier labels (?id:, id:) should be <span>ned. Jun 18, 2022
@github-actions
Copy link

github-actions bot commented Aug 7, 2023

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. The main purpose of this is to keep the issue tracker focused to what is actively being worked on, so that the amount and variety of open yet inactive issues does not overwhelm contributors.

An issue closed as stale is not rejected — further discussion is welcome in its closed state, and it can be resurrected at any time. odoc maintainers regularly check issues that were closed as stale in the past, to see if the time is right to reopen and work on them again. PRs addressing issues closed as stale are as welcome as PRs for open issues. They will be given the same review attention, and any other help.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant