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

API label curation #651

Closed
wants to merge 2 commits into from
Closed

Conversation

lldelisle
Copy link
Contributor

Using #648 (comment) and Yvan's answer.

@lldelisle
Copy link
Contributor Author

ping @bgruening @hexylena

@bgruening
Copy link
Member

If you have time, please change the tool category in the repo. I will merge and for it locally.
If not I try to do that over the weekend.

@hexylena
Copy link
Member

yeah, agreed, we can just correct them, then we wouldn't need extra infrastructure around maintaining disambiguations.

@lldelisle
Copy link
Contributor Author

Then I misunderstood your comment @bgruening : #649 (comment)
You want tools to be in multiple files but not multiple 'tool_panel_section_label', right?

@lldelisle
Copy link
Contributor Author

See #652

@lldelisle lldelisle closed this Nov 16, 2023
@bgruening
Copy link
Member

Correct yes, sorry if I was not clear.

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