Hi,
Am Samstag, den 10. November 2018 um 11:42 Uhr schrieb IOhannes m zmoelnig:
adding generated files to the *repository* itself is a bad idea in general.
???
It is common practice for an abundant number of software projects to put rendered examples in binary format or their documentation in different formats (html, pdf) into dedicated folders of the repo even if the source files of them are distributed as well.
Especially in the case of a pdf and considering its size I don't really see the point in omitting it. If "cleanness" is the issue here, I'd suggest to put up a dedicated, adequately named repo at github with only the pdfs. As pdf is a programming language you'd be putting program sources online ;-)
-- Orm