github: Add Github CI to build doc

GitOrigin-RevId: 62967a6c6a695efa2aef2db3e8151eced8c322e4
CentraleSupelec · Oct 12, 2023 · c045a25 · c045a25
1 parent 753e8cd
commit c045a25
Showing 1 changed file with 25 additions and 0 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -0,0 +1,25 @@
+name: ci
+on:
+    push:
+        branches:
+            - master
+            - main
+permissions:
+    contents: write
+jobs:
+    deploy:
+        runs-on: ubuntu-latest
+        steps:
+            - uses: actions/checkout@v3
+            - uses: actions/setup-python@v4
+              with:
+                  python-version: 3.x
+            - run: echo "cache_id=$(date --utc '+%V')" >> $GITHUB_ENV
+            - uses: actions/cache@v3
+              with:
+                  key: mkdocs-material-${{ env.cache_id }}
+                  path: .cache
+                  restore-keys: |
+                      mkdocs-material-
+            - run: pip install mkdocs-material
+            - run: mkdocs gh-deploy --force