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.

Sign up for GitHub

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

Jump to bottom

Dart: get heuristics #359

Merged
merged 2 commits into from
Nov 7, 2023
Merged

Dart: get heuristics #359

merged 2 commits into from
Nov 7, 2023

Conversation

robertbastian
Copy link
Collaborator

@robertbastian robertbastian commented Nov 7, 2023 •
edited
Loading

Part of #439

@Manishearth
Copy link
Contributor

I kinda feel like these should be handled by backend specific attributes; unless you think this convention is very very strong.

@robertbastian
Copy link
Collaborator Author

It would be nice to have annotations for all these things, but right now this is the easy thing to do...

@robertbastian robertbastian merged commit 39f9b25 into main Nov 7, 2023
5 checks passed
@Manishearth Manishearth deleted the dart branch November 7, 2023 22:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Manishearth Manishearth Manishearth approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@robertbastian @Manishearth