mirror of https://github.com/CGAL/cgal
don't build if round exists
This commit is contained in:
parent
354fdeea53
commit
bd3f64d498
|
|
@ -79,11 +79,17 @@ jobs:
|
||||||
run: |
|
run: |
|
||||||
set -e
|
set -e
|
||||||
PR_NUMBER=${{ steps.get_pr_number.outputs.result }}
|
PR_NUMBER=${{ steps.get_pr_number.outputs.result }}
|
||||||
mkdir -p cgal.github.io/${PR_NUMBER}/${{ steps.get_round.outputs.result }}
|
ROUND=${{ steps.get_round.outputs.result }}
|
||||||
cd build_doc && make -j2 doc && make -j2 doc_with_postprocessing
|
wget cgal.github.io -O tmp.html
|
||||||
cp -r ./doc_output/* ../cgal.github.io/${PR_NUMBER}/${{ steps.get_round.outputs.result }}
|
if $(cat tmp.html |egrep -q "\/$PR_NUMBER\/$ROUND"); then
|
||||||
cd ../cgal.github.io
|
mkdir -p cgal.github.io/${PR_NUMBER}/$ROUND
|
||||||
egrep -v " ${PR_NUMBER}\." index.html > tmp.html
|
cd build_doc && make -j2 doc && make -j2 doc_with_postprocessing
|
||||||
echo "<li><a href=https://cgal.github.io/${PR_NUMBER}/${{ steps.get_round.outputs.result }}/Manual/index.html>Manual for PR ${PR_NUMBER} (${{ steps.get_round.outputs.result }}).</a></li>" >> ./tmp.html
|
cp -r ./doc_output/* ../cgal.github.io/${PR_NUMBER}/$ROUND
|
||||||
mv tmp.html index.html
|
cd ../cgal.github.io
|
||||||
git add ${PR_NUMBER}/${{ steps.get_round.outputs.result }} && git commit -a -m "Add ${PR_NUMBER} round ${{ steps.get_round.outputs.result }}" && git push -u origin master
|
egrep -v " ${PR_NUMBER}\." index.html > tmp.html
|
||||||
|
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 -a -m "Add ${PR_NUMBER} $ROUND" && git push -u origin master
|
||||||
|
else
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue