Synch with remote repo

This commit is contained in:
2025-02-03 10:31:48 +01:00
parent a3ccff4079
commit 32bba4239a
102 changed files with 19584 additions and 19584 deletions

View File

@ -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