Added back the deploy on PR - Clean CI 17

Author: pedrominatel

.github/workflows/docs_build.yml

@@ -42,3 +42,42 @@ jobs:
       with:
         name: docs
         path: docs
+
+  deploy-prod-docs:
+    name: Deploy Documentation on Production
+    runs-on: ubuntu-22.04
+    defaults:
+      run:
+        shell: bash
+    steps:
+    - uses: actions/checkout@v3
+      with:
+        submodules: true
+    - uses: actions/setup-python@v4
+      with:
+        python-version: '3.10'
+    - name: Deploy Documentation
+      env:
+        # Deploy to production server
+        # DOCS_BUILD_DIR: "./docs/_build/"
+        DOCS_DEPLOY_PRIVATEKEY: ${{ secrets.DOCS_PROD_PRIVATEKEY }}
+        DOCS_DEPLOY_PATH: ${{ secrets.DOCS_PROD_PATH }}
+        DOCS_DEPLOY_SERVER: ${{ secrets.DOCS_SERVER }}
+        DOCS_DEPLOY_SERVER_USER: ${{ secrets.DOCS_PROD_USER }}
+        DOCS_DEPLOY_URL_BASE: ${{ secrets.DOCS_PROD_URL_BASE }}
+        # Deploy to preview server
+      run: |
+        sudo apt update
+        sudo apt install python3-pip python3-setuptools
+        source ./docs/utils.sh
+        add_doc_server_ssh_keys $DOCS_DEPLOY_PRIVATEKEY $DOCS_DEPLOY_SERVER $DOCS_DEPLOY_SERVER_USER
+        export GIT_VER=$(git describe --always)
+        echo "PIP install requirements..."
+        pip3 install --user -r ./docs/requirements.txt
+        echo "Building the Docs..."
+        cd ./docs && build-docs -l en
+        echo "Deploy the Docs..."
+        export DOCS_BUILD_DIR=$GITHUB_WORKSPACE/docs/
+        cd $GITHUB_WORKSPACE/docs
+        deploy-docs
+