GitHub Help

[fronobulax]

PR 180 https://github.com/kolmafia/kolmafia/pull/180 seems to have been merged but nothing was built from it.

The red x and the absence of an "announcement" support that hypothesis.

Since I pushed the merge button I feel some responsibility but I can't figure out a) what went wrong and b) how to fix it.

Thanks.

 

[fronobulax]

So I discovered the Actions (as shown above) and see it failed spotless.

So - why did it pass all tests before merge and fail later in build? Do we need to add some tests to the pre-merge?

How do I make the failure go away? Do I reopen the request, make the fix and merge it again? How?

Do I even need to be bothered by this?