Synch with remote repo

2025-02-03 10:31:48 +01:00
parent 5e3f75d66b
commit e358d4ab64
103 changed files with 27163 additions and 27163 deletions
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,12 +1,12 @@
-pages:
-  stage: deploy
-  script:
-    - echo "Deploying pre-built HTML..."
-    - cp -r docs/build/html public  # Copy the pre-built HTML to the public directory
-  artifacts:
-    paths:
-      - public
-  only:
-    changes:
-      - docs/source/**  # Run only if files in docs/source/ change
+pages:
+  stage: deploy
+  script:
+    - echo "Deploying pre-built HTML..."
+    - cp -r docs/build/html public  # Copy the pre-built HTML to the public directory
+  artifacts:
+    paths:
+      - public
+  only:
+    changes:
+      - docs/source/**  # Run only if files in docs/source/ change
      - docs/Makefile