push docs action

Author: antoinedemathelin

.github/workflows/check-docs.yml

@@ -30,6 +30,12 @@ jobs:
     - name: Build documentation
       run: |
         make html
+    - name: Push changes to remote
+      run: |
+        git config --global user.name "github-actions[bot]"
+        git config --global user.email "41898282+github-actions[bot]@users.noreply.github.com"
+        git add docs git commit -m "Update docs"
+        git push
     - uses: actions/upload-artifact@v1
       with:
         name: DocumentationHTML

Makefile

@@ -5,7 +5,7 @@
 # from the environment for the first two.
 SPHINXOPTS    ?=
 SPHINXBUILD   ?= sphinx-build
-SOURCEDIR     = docs/source
+SOURCEDIR     = src_docs
 BUILDDIR      = docs
 
 # Put it first so that "make" without argument is like "make help".

docs/index.html

@@ -7,7 +7,7 @@ REM Command file for Sphinx documentation
 if "%SPHINXBUILD%" == "" (
 	set SPHINXBUILD=sphinx-build
 )
-set SOURCEDIR=docs/source
+set SOURCEDIR=src_docs
 set BUILDDIR=docs
 
 if "%1" == "" goto help