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

[nix] ghc925 -> ghc927 #4962

Merged
merged 1 commit into from
Mar 10, 2023
Merged

[nix] ghc925 -> ghc927 #4962

merged 1 commit into from
Mar 10, 2023

Conversation

angerman
Copy link
Contributor

After we bumped GHC to 9.2.7 in GHA, let's bump it to 9.2.7 in nix as well.

@angerman angerman requested review from a team, deepfire, mgmeier and fmaste as code owners March 10, 2023 03:27
@angerman angerman enabled auto-merge March 10, 2023 06:32
@andreabedini andreabedini self-requested a review March 10, 2023 06:33
Copy link
Contributor

@andreabedini andreabedini left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍 ✅ LGTM

@angerman angerman added this pull request to the merge queue Mar 10, 2023
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 10, 2023
@angerman angerman added this pull request to the merge queue Mar 10, 2023
@angerman angerman removed this pull request from the merge queue due to a manual request Mar 10, 2023
@angerman angerman enabled auto-merge March 10, 2023 07:44
@angerman angerman added this pull request to the merge queue Mar 10, 2023
Merged via the queue into master with commit d91516b Mar 10, 2023
@iohk-bors iohk-bors bot deleted the nix/ghc925-927 branch March 10, 2023 08:14
@michaelpj
Copy link
Contributor

ci/pr/nix/required FAILED

How did this merge? Looks like the dev shell is now uncached :(

@jbgi
Copy link
Contributor

jbgi commented Mar 10, 2023

How did this merge? Looks like the dev shell is now uncached :(

because nix builds are now not required (team decision): #4923 (comment)

@michaelpj
Copy link
Contributor

Then it's essentially guaranteed to be broken and you might as well delete it all 🤷 That's a pretty big foot gun for contributors.

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.

4 participants