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

simplify binder handling #83

Merged
merged 2 commits into from
Mar 30, 2024
Merged

simplify binder handling #83

merged 2 commits into from
Mar 30, 2024

Conversation

ZuseZ4
Copy link
Member

@ZuseZ4 ZuseZ4 commented Mar 30, 2024

No description provided.

@ZuseZ4
Copy link
Member Author

ZuseZ4 commented Mar 30, 2024

@jedbrown Not sure about the caching you added, but I assume there aren't any reasons to not set up the CI to cancel previous CI runs if we push to a branch?

@ZuseZ4 ZuseZ4 merged commit 7ac8be7 into master Mar 30, 2024
9 of 12 checks passed
@ZuseZ4 ZuseZ4 deleted the imprv-lifetime-erasure branch March 30, 2024 03:00
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.

1 participant