diff --git a/.github/workflows/build_doc.yml b/.github/workflows/build_doc.yml index 11112e5a3b9..2591ff53482 100644 --- a/.github/workflows/build_doc.yml +++ b/.github/workflows/build_doc.yml @@ -81,7 +81,7 @@ jobs: done cp -r ./doc_output/Manual ../cgal.github.io/${PR_NUMBER}/$ROUND cd ../cgal.github.io - egrep -v " ${PR_NUMBER}\." index.html > tmp.html + egrep -v " ${PR_NUMBER}\." index.html > tmp.html || true echo "
  • Manual for PR ${PR_NUMBER} ($ROUND).
  • " >> ./tmp.html mv tmp.html index.html git add ${PR_NUMBER}/$ROUND && git commit -q --amend -m "base commit" && git push -q -f -u origin master diff --git a/.github/workflows/delete_doc.yml b/.github/workflows/delete_doc.yml index 6a8d6bc15be..2e3594a12d6 100644 --- a/.github/workflows/delete_doc.yml +++ b/.github/workflows/delete_doc.yml @@ -18,7 +18,7 @@ jobs: git clone https://maxGimeno:${{ secrets.PUSH_TO_CGAL_GITHUB_IO_TOKEN }}@github.com/CGAL/cgal.github.io.git --depth=5 PR_NUMBER=$(python -c "import json; import os; y = json.load(open(os.environ['GITHUB_EVENT_PATH'])); print(y[\"number\"])") cd cgal.github.io/ - egrep -v " ${PR_NUMBER}\." index.html > tmp.html + egrep -v " ${PR_NUMBER}\." index.html > tmp.html || true if [ -n "$(diff -q ./index.html ./tmp.html)" ]; then mv tmp.html index.html #git commit -a -m "Remove ${PR_NUMBER}" && git push -u origin master