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

CI: replace centos:7 container by redhat/ubi9:latest #327

Merged
merged 6 commits into from
Nov 19, 2024
Merged

Conversation

andreasabel
Copy link
Member

@andreasabel andreasabel commented Nov 19, 2024

Github disabled workflow ci.yml because its job centos7 perpetually failed (Centos EOL).
This replaces the centos:7 image by redhat/ubi9:latest.

SQUASH this PR upon merge.

@andreasabel andreasabel reopened this Nov 19, 2024
@Bodigrim
Copy link
Contributor

CentOS 9 is not as much different from other distros as CentOS 7 used to be, so I’m personally inclined to drop this CI job if it’s nontrivial to set up.

@andreasabel
Copy link
Member Author

andreasabel commented Nov 19, 2024

Somewhere it has been said that redhat/ubi9 would be a replacement for centos. It seems to work with minimal changes (dropping the obsolote ncurses-compat-libs).

ci.yml succeeds again.

@andreasabel andreasabel changed the title CI: try centos:9 container CI: replace centos:7 container by redhat/ubi9:latest Nov 19, 2024
@andreasabel andreasabel requested a review from Bodigrim November 19, 2024 20:34
@Bodigrim Bodigrim merged commit 283160b into master Nov 19, 2024
45 of 46 checks passed
@Bodigrim Bodigrim deleted the ci-centos9 branch November 19, 2024 21:38
@Bodigrim
Copy link
Contributor

Thanks!

@Bodigrim
Copy link
Contributor

Arrrgh, I forgot to squash, will push --force in a moment.

@Bodigrim
Copy link
Contributor

Apparently even my access level is not enough to push --force, I think a few repos were branch-protected by GitHub support a few years ago. Let's leave it as a monument to my inability to read.

@andreasabel
Copy link
Member Author

Ok, no worries. Been there, done that. :-D

Thanks!

@andreasabel
Copy link
Member Author

I wish github would have a special label like "squash me" that one would have to remove first if one wanted to merge other than squash... In the Agda repo, I created the "pr: squash me" label, but it is easy to overlook, does not have the magic I want it to have...

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.

2 participants