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

Cleanup terms and definitions #24

Closed
ClemensLinnhoff opened this issue Jun 26, 2024 · 0 comments · Fixed by #25
Closed

Cleanup terms and definitions #24

ClemensLinnhoff opened this issue Jun 26, 2024 · 0 comments · Fixed by #25
Assignees
Labels
isType:Bug An issue that contains contradictions or errors in the standard.

Comments

@ClemensLinnhoff
Copy link
Collaborator

ClemensLinnhoff commented Jun 26, 2024

Describe the bug
Terms and definitions got merged in an intermediate state. Now the file needs to be cleaned up. See comments in #18

@ClemensLinnhoff ClemensLinnhoff added the isType:Bug An issue that contains contradictions or errors in the standard. label Jun 26, 2024
@ClemensLinnhoff ClemensLinnhoff self-assigned this Jun 26, 2024
@ClemensLinnhoff ClemensLinnhoff linked a pull request Jun 26, 2024 that will close this issue
2 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
isType:Bug An issue that contains contradictions or errors in the standard.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant