Merge pull request #5126 from maxGimeno/CI-doc_fix-maxGimeno

CI: auto doc fix
This commit is contained in:
Laurent Rineau 2020-10-28 11:15:01 +01:00 committed by GitHub
commit 6167c96bf9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 2 additions and 2 deletions

View File

@ -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 "<li><a href=https://cgal.github.io/${PR_NUMBER}/$ROUND/Manual/index.html>Manual for PR ${PR_NUMBER} ($ROUND).</a></li>" >> ./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

View File

@ -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