Remove doc.pdf from Repository #332
Description
In GitLab by @Jonas_schwab on Nov 28, 2025, 18:32 UTC:
I recently added a something to the pipeline that auto-commits doc.pdf if there is any difference between the one in the repository and the one built in the pipeline. This was to ensure that the version in the repository is always up to date.
This feature turned out to be more annoying than anticipated, but it might also make sense to not keep doc.pdf in the repo, because keeping track of a ~2MB binary might unnecessarily inflate the repository size over time.
I suggest to gitignore Documentation/doc.pdf and reference the doc.pdf as pipeline artifacts (as it is done in most places already).
Assignees: Jonas_schwab
Migrated from GitLab: https://git.physik.uni-wuerzburg.de/ALF/ALF/-/issues/332