songsenand
/
cgal
mirror of https://github.com/CGAL/cgal
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Add a github manip

This commit is contained in:
Maxime Gimeno 2020-09-08 14:54:22 +02:00
parent 9cae0bdad7
commit 08600afd72
2 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.github/workflows/build_doc.yml vendored
View File

@ -46,4 +46,5 @@ jobs:
set -e set -e
cd build_doc && make -j2 doc && make -j2 doc_with_postprocessing cd build_doc && make -j2 doc && make -j2 doc_with_postprocessing
PR_NUMBER=$(python -c "import json; import os; y = json.load(open(os.environ['GITHUB_EVENT_PATH'])); print(y[\"number\"])") PR_NUMBER=$(python -c "import json; import os; y = json.load(open(os.environ['GITHUB_EVENT_PATH'])); print(y[\"number\"])")
rsync --compress -a doc_output/* ${{ secrets.ids }}/pr_doc/${PR_NUMBER}/ rsync --compress -a doc_output/* ${{ secrets.ids }}/cgal.github.io/${PR_NUMBER}/
ssh mgimeno@cgal.geometryfactory.com "cd /home/mgimeno/public_html/cgal.github.io && git add ${PR_NUMBER} && git commit -a -m 'Add a new directory' && git push origin master"

4
.github/workflows/delete_doc.yml vendored
View File

@ -12,6 +12,7 @@ jobs:
- uses: actions/checkout@v2.0.0 - uses: actions/checkout@v2.0.0
- name: delete directory - name: delete directory
run: | run: |
set -x
mkdir -p ~/.ssh mkdir -p ~/.ssh
( (
cat <<EOF cat <<EOF
@ -32,5 +33,6 @@ jobs:
EOF EOF
)>> ~/.ssh/known_hosts )>> ~/.ssh/known_hosts
PR_NUMBER=$(python -c "import json; import os; y = json.load(open(os.environ['GITHUB_EVENT_PATH'])); print(y[\"number\"])") PR_NUMBER=$(python -c "import json; import os; y = json.load(open(os.environ['GITHUB_EVENT_PATH'])); print(y[\"number\"])")
ssh mgimeno@cgal.geometryfactory.com rm -rf /home/mgimeno/public_html/pr_doc/${PR_NUMBER} #ssh mgimeno@cgal.geometryfactory.com rm -rf /home/mgimeno/public_html/cgal.github.io/${PR_NUMBER}
ssh mgimeno@cgal.geometryfactory.com "cd /home/mgimeno/public_html/cgal.github.io && rm -rf ${PR_NUMBER} && git rm -r ${PR_NUMBER} && git commit -a -m 'Remove a directory' && git push origin master"