Skip to content

Commit

Permalink
ci: show more info on checkout
Browse files Browse the repository at this point in the history
ci skip
  • Loading branch information
biojppm committed Aug 14, 2024
1 parent 9811a45 commit f8253a3
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 15 deletions.
6 changes: 3 additions & 3 deletions .github/workflows/clang.yml
Original file line number Diff line number Diff line change
Expand Up @@ -159,10 +159,10 @@ jobs:
- name: checkout
run: |
set -x
echo $GITHUB_REF
echo $GITHUB_HEAD_REF
echo GITHUB_REF=$GITHUB_REF
echo GITHUB_HEAD_REF=$GITHUB_HEAD_REF
branch=${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}} # https://stackoverflow.com/questions/58033366
echo $branch
echo branch=$branch
git init -q .
git config --system --add safe.directory '*' # needed for running in the docker image. see https://github.com/actions/checkout/issues/1169
git remote add origin $GITHUB_SERVER_URL/$GITHUB_REPOSITORY
Expand Down
24 changes: 12 additions & 12 deletions .github/workflows/gcc.yml
Original file line number Diff line number Diff line change
Expand Up @@ -53,10 +53,10 @@ jobs:
- name: checkout
run: |
set -x
echo $GITHUB_REF
echo $GITHUB_HEAD_REF
echo GITHUB_REF=$GITHUB_REF
echo GITHUB_HEAD_REF=$GITHUB_HEAD_REF
branch=${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}} # https://stackoverflow.com/questions/58033366
echo $branch
echo branch=$branch
git init -q .
git config --system --add safe.directory '*' # needed for running in the docker image. see https://github.com/actions/checkout/issues/1169
git remote add origin $GITHUB_SERVER_URL/$GITHUB_REPOSITORY
Expand Down Expand Up @@ -109,10 +109,10 @@ jobs:
- name: checkout
run: |
set -x
echo $GITHUB_REF
echo $GITHUB_HEAD_REF
echo GITHUB_REF=$GITHUB_REF
echo GITHUB_HEAD_REF=$GITHUB_HEAD_REF
branch=${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}} # https://stackoverflow.com/questions/58033366
echo $branch
echo branch=$branch
git init -q .
git config --system --add safe.directory '*' # needed for running in the docker image. see https://github.com/actions/checkout/issues/1169
git remote add origin $GITHUB_SERVER_URL/$GITHUB_REPOSITORY
Expand Down Expand Up @@ -193,10 +193,10 @@ jobs:
- name: checkout
run: |
set -x
echo $GITHUB_REF
echo $GITHUB_HEAD_REF
echo GITHUB_REF=$GITHUB_REF
echo GITHUB_HEAD_REF=$GITHUB_HEAD_REF
branch=${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}} # https://stackoverflow.com/questions/58033366
echo $branch
echo branch=$branch
git init -q .
git config --system --add safe.directory '*' # needed for running in the docker image. see https://github.com/actions/checkout/issues/1169
git remote add origin $GITHUB_SERVER_URL/$GITHUB_REPOSITORY
Expand Down Expand Up @@ -305,10 +305,10 @@ jobs:
- name: checkout
run: |
set -x
echo $GITHUB_REF
echo $GITHUB_HEAD_REF
echo GITHUB_REF=$GITHUB_REF
echo GITHUB_HEAD_REF=$GITHUB_HEAD_REF
branch=${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}} # https://stackoverflow.com/questions/58033366
echo $branch
echo branch=$branch
git init -q .
git config --system --add safe.directory '*' # needed for running in the docker image. see https://github.com/actions/checkout/issues/1169
git remote add origin $GITHUB_SERVER_URL/$GITHUB_REPOSITORY
Expand Down

0 comments on commit f8253a3

Please sign in to comment.