ignore remote changes to a specific, ignored file

Question

In our git repository for a latex project, pdf files are set to be ignored. Some still manage to push the compiled pdf, which makes the occasional pull a conflict between my local and the remote pdf, as it returns: "Your local changes to the following files would be overwritten by merge"

Is there a git feature that does this: "always ignore remote changes to this file", ideally synced with what's listed in the .gitignore?

I could solve this
(1) by agreeing that no ones pushes files that are on the ignore list and reverting the corresponding changes (several mixed commits by now),
(2a) by ignoring my changes via an alias for rm that-file.pdf && git pull or similarly
(2b) by backing up that file and overwriting the pulled change. Or
(3) I could always build my latex-project into a build folder, and remember that when I need the current pdf.

Answers for similar problems:

• pushing the pdf removal for everyone is a good approach, but I don't want to cause remote changes in that matter (let us assume the person pushing the PDF is happy to be able to open the file from the web-interface, too)
• force git pull via git fetch --all && git reset --hard origin/master would not only overwrite my pdf (which is ok, although I'd prefer to ignore the remote change), but I'd risk losing local changes out of the .gitignore scope, too.
• --assume-unchanged is getting in the right direction, but cannot handle regular updates to the remote pdf
• this question is similar, but asks to skip all conflicting remote updates (while I appreciate a pull failing due to a conflict, as long it doesn't concern a file on the ignore list)

edit:

git hooks are potentially helpful here (see comments below).

• Unfortunately, pre-pull hooks don't exist although they could help individuals keeping a normal workflow without asking other people anything.
• A server-side hook can reject the commit with an error message and maybe it can also just rename the commited pdf
• A client-side pre-commit hook can help to avoid commits not respecting the .gitignore

Answer 1

Every Git repository clone is private and you cannot stop anyone from doing anything they want with their own personal private clone. That leaves you with only two guaranteed options:

• Set up some sort of controls on a centralized repository to which people push (e.g., GitHub's "protected branches"); and/or
• Don't take their commits as-is with git pull. Avoid git pull entirely. Use git fetch, inspect the incoming commits, and reject (or add fixup commits to) their commits if they are incorrect.

You can ask collaborators to install correct .gitignore files and/or pre-commit hooks, but they're equally free to ignore your pleas. Once a bad commit exists, it literally cannot be fixed: at most, you can make a new commit that's like the bad commit, but improved, either as a replacement (which is generally a headache but may eventually save space in the repository as the PDFs may be large) or as an add-on commit (generally safer, Git does the right things here).

Here's an example command sequence that adds a fixup commit when Person X (the bad guy) commits some pdf file that he should not have:

• git fetch: get their new commit(s)

• git log --stat ..@{u}: observe what they did

• If they did it wrong:

  git worktree add -b fix-yet-another-person-x-screwup ../fixup @{u}
  pushd ../fixup
  git rm wrongfile.pdf
  git commit -m 'rm incorrectly added pdf'
  git push origin HEAD:whatever-the-branch-is
  popd
  git fetch
  

  Assuming all has gone well at this point, you can now git worktree remove the added working tree (../fixup in this example) and it is now safe to run git merge as usual.

You can even build an automated system to check for bad commits (perhaps only bothering to check the ones from known bad guys).

Note that Person X won't see your branch names unless you show them to him, so you can be as snarky as you like with them. (But beware of accidentally showing them, which is pretty easy to do by mistake.)