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 /src/theory/arith/arith_msum.cpp | |
| 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 'src/theory/arith/arith_msum.cpp')
0 files changed, 0 insertions, 0 deletions