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

panlint: Allow whitespace between annotation name and body #262

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

jrha
Copy link
Member

@jrha jrha commented Oct 24, 2024

This is contrary to the documentation, but accepted by the compiler.

@jrha jrha added the panlint label Oct 24, 2024
@ned21
Copy link
Contributor

ned21 commented Oct 27, 2024

Is the doc in this same repo? In which case, should this RR also contain a commit fixing the docs?

I have a feeling that since we're still using the last released version of panlint rather than HEAD we haven't been enforcing this... I can imagine it's annoying to enforce so can see why you'd want to allow it to reduce the toil of ensuring compliance.

This is contrary to the documentation, but accepted by the compiler.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Development

Successfully merging this pull request may close these issues.

2 participants