Closed mgeier closed 1 year ago
TBH, I don't think that anybody is reading those docs anyway, right?
This would reduce the CI time significantly. Building the docs only takes about 20 seconds, but uploading hundreds of HTML files takes 2.5 minutes.
If needed, they can be built locally with make doc.
make doc
The HTML version of the user manual is still built, but this is no problem because it's much faster (a few seconds).
TBH, I don't think that anybody is reading those docs anyway, right?
This would reduce the CI time significantly. Building the docs only takes about 20 seconds, but uploading hundreds of HTML files takes 2.5 minutes.
If needed, they can be built locally with
make doc.The HTML version of the user manual is still built, but this is no problem because it's much faster (a few seconds).