Rename the master branch to main

This commit is contained in:
Martin Robinson 2023-11-27 14:03:16 +01:00
parent 7bcb25c85c
commit 23add0c1e5
14 changed files with 47 additions and 51 deletions

View file

@ -13,13 +13,9 @@ jobs:
run: echo "PR_FETCH_DEPTH=$(( ${{ github.event.pull_request.commits }} + 1 ))" >> "${GITHUB_ENV}"
- name: Check out shallow servo PR
run: |
mkdir servo
git clone --depth 1 ${{ github.event.repository.clone_url}} servo
cd servo
git init -b main
git remote add origin ${{ github.event.repository.clone_url}}
git fetch origin pull/${{ github.event.pull_request.number}}/head:pr --depth ${{ env.PR_FETCH_DEPTH }}
git fetch origin master:master --depth 1
git checkout master
- name: Check out wpt
uses: actions/checkout@v3
with: