3737 echo ">"
3838 git diff-index --quiet HEAD & git status -s
3939 echo "<"
40- echo "TO_BE_CANCELLED =$(if [[ $(git diff-index --quiet HEAD & git status -s) ]]; then echo "false"; else echo "true"; fi)" >> $GITHUB_ENV
41- echo "$TO_BE_CANCELLED "
40+ echo "COMPILER_TO_BE_CANCELLED =$(if [[ $(git diff-index --quiet HEAD & git status -s) ]]; then echo "false"; else echo "true"; fi)" >> $GITHUB_ENV
41+ echo "$COMPILER_TO_BE_CANCELLED "
4242 - name : Copy docs and consolidate links to ${REPO_TUTORIAL_DEST} Repository
43- if : ${{ env.TO_BE_CANCELLED == 'false' }}
4443 run : |
4544 cp -rf ${REPO_COMPILER_SOURCE}/documentation/* ${REPO_TUTORIAL_DEST}/
4645 cd ${REPO_TUTORIAL_DEST}
@@ -52,28 +51,26 @@ jobs:
5251 echo ">"
5352 git diff-index --quiet HEAD & git status -s
5453 echo "<"
55- echo "TO_BE_CANCELLED =$(if [[ $(git diff-index --quiet HEAD & git status -s) ]]; then echo "false"; else echo "true"; fi)" >> $GITHUB_ENV
56- echo "$TO_BE_CANCELLED "
54+ echo "TUTORIAL_TO_BE_CANCELLED =$(if [[ $(git diff-index --quiet HEAD & git status -s) ]]; then echo "false"; else echo "true"; fi)" >> $GITHUB_ENV
55+ echo "$TUTORIAL_TO_BE_CANCELLED "
5756 - name : setup git user
58- if : ${{ env.TO_BE_CANCELLED == 'false' }}
57+ if : ${{ env.COMPILER_TO_BE_CANCELLED == 'false' || env.TUTORIAL_TO_BE_CANCELLED == 'false' }}
5958 run : |
6059 git config --global user.email ${BUILD_USER_EMAIL}
6160 git config --global user.name ${BUILD_USER}
6261 - name : Sync Wiki
63- if : ${{ env.TO_BE_CANCELLED == 'false' }}
62+ if : ${{ env.COMPILER_TO_BE_CANCELLED == 'false' }}
6463 run : |
6564 cd ${REPO_COMPILER_DEST}
66- git checkout master
6765 git status
6866 git add .
6967 git commit -m "${REPO_COMPILER_SOURCE} documentation | GitHub Actions $GITHUB_WORKFLOW $GITHUB_RUN_NUMBER"
7068 git remote add origin-wiki "https://${BUILD_USER}:${BUILD_USER_PASSWD}@github.com/${ORG}/${REPO_COMPILER_DEST}.git"
7169 git push origin-wiki master
7270 - name : Sync Wiki ${REPO_TUTORIAL_DEST} Repository
73- if : ${{ env.TO_BE_CANCELLED == 'false' }}
71+ if : ${{ env.TUTORIAL_TO_BE_CANCELLED == 'false' }}
7472 run : |
7573 cd ${REPO_TUTORIAL_DEST}
76- git checkout master
7774 git pull
7875 git status
7976 git add .
0 commit comments