diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-05-26 08:10:51 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-26 06:10:51 +0000 |
| commit | 22d05234d9a4a98ad715d6e2d6cb1616592fd2b5 (patch) | |
| tree | e87106fa825520c03a8fadc7150f4d06f21d2c10 /.github | |
| parent | 8bdef44df0876840a9fb34e7bd820b0eee7c9700 (diff) | |
Reduce size of sphinx-gh output (#6601)
This PR reduces the disk size of the docs generated by make sphinx-gh.
Apart from reformatting the cmake source, we now not only remove the _sources folder, but also .doctrees (essentially the sphinx cache) and _static/fonts/ (the fonts that are actually used live in _static/css/fonts).
In combination, this now reduces the disk size from about 20MB (sphinx) to less than 6MB (sphinx-gh).
Furthermore this PR only uploads the generated documentation if it differs from whatever we currently have for master.
This is relevant to make the docs-ci repository smaller (which already has more than 5GB...)
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/docs_cleanup.yml | 10 | ||||
| -rw-r--r-- | .github/workflows/docs_upload.yml | 20 |
2 files changed, 21 insertions, 9 deletions
diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml index 67b5f6b4a..f56a0f595 100644 --- a/.github/workflows/docs_cleanup.yml +++ b/.github/workflows/docs_cleanup.yml @@ -4,8 +4,9 @@ on: - cron: '0 1 * * SUN' jobs: - build: + docs-cleanup: runs-on: ubuntu-latest + if: github.repository == 'cvc5/cvc5' steps: - name: Install Packages run: | @@ -58,6 +59,11 @@ jobs: python3 genindex.py git add README.md - git commit -m "Update README.md" + if git diff --cached --exit-code + then + echo "Nothing changed" + else + git commit -m "Update README.md" + fi git push -f diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml index 356337de6..7346371e3 100644 --- a/.github/workflows/docs_upload.yml +++ b/.github/workflows/docs_upload.yml @@ -75,15 +75,21 @@ jobs: if [ -n "$NAME" ]; then mv docs-new target/docs-$NAME-$HASH cd target/ - rm -f docs-$NAME - ln -s docs-$NAME-$HASH docs-$NAME - git add docs-$NAME docs-$NAME-$HASH - python3 genindex.py - git add README.md - git commit -m "Update docs for $NAME" + if diff -r target/docs-master/ target/docs-$NAME-$HASH + then + echo "Ignored run, documentation is the same as for current master" + else + rm -f docs-$NAME + ln -s docs-$NAME-$HASH docs-$NAME + git add docs-$NAME docs-$NAME-$HASH - git push + python3 genindex.py + git add README.md + git commit -m "Update docs for $NAME" + + git push + fi else echo "Ignored run" fi |