Do not display auto-generated files in GitHub PR diffs

[Zimmi48]

GitHub supports marking some committed files as auto-generated, in which case, they are not shown by default in PR diffs (as in https://github.com/conda-forge/coq-feedstock/pull/13/files). If we want to use this feature, the trick is to pass linguist-generated=true in .gitattributes, as shown here.

[Zimmi48]

We need a system to be able to tell generate.sh that some file has been manually modified and should not be overwritten when regenerating from the templates. With @CohenCyril, we have considered using the header comments as a signal whether the file is auto-generated or not, but this doesn't work for files which do not support header comments like dune-project. So instead, we've decided that we could rely on these linguist-generated=true annotations in .gitattributes. When someone modifies an auto-generated file, they would need to remove it from the list and generate.sh file would detect that it exists but isn't listed and would stop updating it (printing a notice instead).