From 94f1c7cbe9ac940729000a97ce3db4b9420f2ccc Mon Sep 17 00:00:00 2001
From: Maxime Gimeno <maxime.gimeno@gmail.com>
Date: Wed, 9 Sep 2020 11:07:00 +0200
Subject: [PATCH] update index too

---
 .github/workflows/build_doc.yml  | 19 +++++++++++++++----
 .github/workflows/delete_doc.yml |  7 +++++++
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/build_doc.yml b/.github/workflows/build_doc.yml
index 666a68801ea..c6d330a035d 100644
--- a/.github/workflows/build_doc.yml
+++ b/.github/workflows/build_doc.yml
@@ -41,14 +41,25 @@ jobs:
     - name: configure all
       run: |
         git clone git@github.com:CGAL/cgal.github.io.git
-        mkdir build_doc && cd build_doc && cmake ../Documentation/doc
+        mkdir -p build_doc && cd build_doc && cmake ../Documentation/doc
     - name: Upload Doc
       run: |
         set -e
         PR_NUMBER=$(python -c "import json; import os; y = json.load(open(os.environ['GITHUB_EVENT_PATH'])); print(y[\"number\"])")
-        mkdir cgal.github.io/${PR_NUMBER}
+        mkdir -p cgal.github.io/${PR_NUMBER}
         cd build_doc && make -j2 doc && make -j2 doc_with_postprocessing
-        mv ./doc_output/* ../cgal.github.io/${PR_NUMBER}/
+        cp -r ./doc_output/* ../cgal.github.io/${PR_NUMBER}/
+        cd ../cgal.github.io
+        INDEX_EXISTS=""
+        while IFS= read -r line
+        do
+           if [[ $line == *" ${PR_NUMBER}."* ]]; then
+             INDEX_EXISTS="TRUE"
+           fi
+        done < "index.html"
+        if [ -z "$INDEX_EXISTS" ]; then 
+          echo "<li><a href=https://cgal.github.io/${PR_NUMBER}/Manual/index.html>Manual for PR ${PR_NUMBER}.</a></li>" >> ./index.html
+        fi
         #rsync --compress -a doc_output/* ${{ secrets.ids }}/cgal.github.io/${PR_NUMBER}/
-        cd ../cgal.github.io && git add ${PR_NUMBER} && git commit -a -m "Add ${PR_NUMBER}" && git push -u origin master
+        git add ${PR_NUMBER} && git commit -a -m "Add ${PR_NUMBER}" && git push -u origin master
         #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"
diff --git a/.github/workflows/delete_doc.yml b/.github/workflows/delete_doc.yml
index d3cad05ef79..91a4f5d6a08 100644
--- a/.github/workflows/delete_doc.yml
+++ b/.github/workflows/delete_doc.yml
@@ -36,6 +36,13 @@ jobs:
          git clone git@github.com:CGAL/cgal.github.io.git
          PR_NUMBER=$(python -c "import json; import os; y = json.load(open(os.environ['GITHUB_EVENT_PATH'])); print(y[\"number\"])")
          cd cgal.github.io/
+         while IFS= read -r line
+         do
+            if [[ $line != *" ${PR_NUMBER}."* ]]; then
+              echo "$line" >> tmp.html
+            fi
+         done < "index.html"
+         mv tmp.html index.html
          git rm -r ${PR_NUMBER} && git commit -a -m "Remove ${PR_NUMBER}" && git push -u origin master
          
          #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"