-
Notifications
You must be signed in to change notification settings - Fork 105
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
Add TODOs related to #429 and quotes to safety comments. #433
Add TODOs related to #429 and quotes to safety comments. #433
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Awesome, thank you so much for these! This is exactly what we're looking for. A few minor style nits, but the content is good.
d0e7316
to
51d2016
Compare
Thank you for your feedback! Don't worry about being picky, that's the kind of thing I'm looking to learn :) I think I've addressed all of your comments, if there is anything else do let me know. Question: The code still contains safety comments (starting with //SAFETY:) that are not wrapped in the safety_comment! macro. Is this intentional and if so what is the purpose of the differentiation? (I had some git problems, but think they are fixed? (accidentally merged upstream changes through the github gui). If anything is off do let me know and I'll try to figure it out.) |
Awesome, thanks! I'll try to get to these soon.
Yeah, that's intentional. Normally you'd just put a Lines 24 to 29 in 9ce05f8
Seems fine to me 🤷♂️ We have this repo configured to squash all commits into a single one when a PR is merged, so it probably doesn't make much of a difference (perhaps with the exception that the resulting commit message will include a summary of each commit that was included in the PR). Personally my flow is to always just edit the commit and then force push, but whatever flow works for you is fine. |
Thanks for the explanation of the safety_comment macro, that makes sense! I'll adopt the same push -f method for edits in the future :) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay, this looks great! Just a few tiny nits, but as soon as these are resolved, I'll approve it 🙂
51d2016
to
0795819
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Added your changes! I'll make sure to keep spacing and use [] when quoting in the middle of a sentence. merged all commits into one now as well.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks again for all your work on this! I cleaned a few things up (deleting spurious extra newlines and such) and it's ready to merge.
Apologies for not getting back to you sooner, thanks for taking the time! |
No worries at all! I was just going back and cleaning up old PRs and I figured it was silly to ask you to do a few obvious edits when I was doing it already 🙂 |
While reading through some of the code I added some quotes and TODOs here and there related to #429.