Skip to content

fix: use https://git.savannah.gnu.org/git/bash instead of https://github.com/bolinfest/bash#13057

Open
bolinfest wants to merge 1 commit intomainfrom
pr13057
Open

fix: use https://git.savannah.gnu.org/git/bash instead of https://github.com/bolinfest/bash#13057
bolinfest wants to merge 1 commit intomainfrom
pr13057

Conversation

@bolinfest
Copy link
Collaborator

@bolinfest bolinfest commented Feb 27, 2026

Historically, we cloned the Bash repo from https://github.com/bminor/bash, but for whatever reason, it was removed at some point.

I had a local clone of it, so I pushed it to https://github.com/bolinfest/bash so that we could continue running our CI job. I did this in #9563, and as you can see, I did not tamper with the commit hash we used as the basis of this build.

Using a personal fork is not great, so this PR changes the CI job to use what appears to be considered the source of truth for Bash, which is https://git.savannah.gnu.org/git/bash.git.

Though in testing this out, it appears this Git server does not support the combination of git clone --depth 1 https://git.savannah.gnu.org/git/bash and git fetch --depth 1 origin a8a1c2fac029404d3f42cd39f5a20f24b6e4fe4b, as it fails with the following error:

error: Server does not allow request for unadvertised object a8a1c2fac029404d3f42cd39f5a20f24b6e4fe4b

so unfortunately this means that we have to do a full clone instead of a shallow clone in our CI jobs, which will be a bit slower.

Also updated codex-rs/shell-escalation/README.md to reflect this change.

@bolinfest bolinfest enabled auto-merge (squash) February 27, 2026 21:07
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