diff options
| author | Sebastian Berg <sebastian@sipsolutions.net> | 2021-03-07 15:05:35 -0600 |
|---|---|---|
| committer | Sebastian Berg <sebastian@sipsolutions.net> | 2021-03-07 16:21:31 -0600 |
| commit | 5631e8ee5aeea8fe645ee46aa12f76ecff1badf2 (patch) | |
| tree | eed854906503d432e3e03117a8e946f21dd746aa | |
| parent | 516a0ce17153ffd3153bc9427869bff2b58e329a (diff) | |
| download | numpy-5631e8ee5aeea8fe645ee46aa12f76ecff1badf2.tar.gz | |
CI: Do not pass original branch name to `git branch -m main`
Should fix the current failure that "master" does not exist.
I am a bit curious why master does not exist, maybe the CircleCI
git is set up to use some other default.
Move the branch rename to after the commit, to make sure that
the fact that the branch is empty (and `git branch` also)
cannot influence the result.
[ci-skip]
| -rwxr-xr-x | tools/ci/push_docs_to_repo.py | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/ci/push_docs_to_repo.py b/tools/ci/push_docs_to_repo.py index 00c4f7074..058f748ec 100755 --- a/tools/ci/push_docs_to_repo.py +++ b/tools/ci/push_docs_to_repo.py @@ -45,7 +45,9 @@ workdir = tempfile.mkdtemp() os.chdir(workdir) run(['git', 'init']) -run(['git', 'branch', '-m', 'master', 'main']) +# ensure the working branch is called "main" +# (`--initial-branch=main` appared to have failed on older git versions): +run(['git', 'checkout', '-b', 'main']) run(['git', 'remote', 'add', 'origin', args.remote]) run(['git', 'config', '--local', 'user.name', args.committer]) run(['git', 'config', '--local', 'user.email', args.email]) |