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

Some tests and cleanup for glueings. #1613

Merged
merged 3 commits into from
Oct 12, 2022

Conversation

HechtiDerLachs
Copy link
Collaborator

No description provided.

@simonbrandhorst simonbrandhorst enabled auto-merge (squash) October 11, 2022 17:54
@HechtiDerLachs
Copy link
Collaborator Author

We should probably be a bit careful with the automerge. I just saw that, due to the bug in the documentation, our other PR is also still not merged. I might have to rebase on that, eventually.

@simonbrandhorst
Copy link
Collaborator

Alright, I will turn off the automerge for now.

@thofma thofma closed this Oct 11, 2022
@thofma thofma reopened this Oct 11, 2022
@simonbrandhorst simonbrandhorst merged commit c6fced6 into oscar-system:master Oct 12, 2022
@simonbrandhorst simonbrandhorst deleted the glueing_cleanup branch October 12, 2022 05:35
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.

None yet

3 participants