Bump to 0.10.2 #1515
Merged
Bump to 0.10.2 #1515
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
It has been a month since the last release and there was a breaking bump in Hecke that I would like to propagate.
|
@benlorenz I have seen https://github.com/oscar-system/Oscar.jl/runs/8010583830?check_suite_focus=true#step:5:193 fail for a few PRs recently. |
|
I will merge later today if there are no objections. |
Thanks for noticing and the ping, that is quite weird, we will have a look and add some debugging output to check the timings on github actions. For most of the testgroups github actions needs about twice as long as munk (with julia nightly). But this timings testgroup takes more than 4 times as long. Edit: this should disappear once #1517 is merged |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
It has been a month since the last release and there was a breaking version bump in Hecke that I would like to propagate.