Server-side preventing some files from being overwritten

Hi *,

is there a way, for example with some sort of pre-receive hook, to prevent some files from being overwritten by a push?

Use case:

In some project, we use Flyway to manage the database schema, and Jenkins to automatically build master’s HEAD after each push (and install it, thus activating the schema files almost immediately). Now, I wish to prevent coworkers from changing anything in the SQL subdirectory that has ever been pushed, forcing them to push new SQL files with ALTER statements instead. (Yes, I am aware this will likely make me even less liked. No, this is not an issue.)

As for the comparison, only the changes between the previous HEAD of master and the new HEAD of master after the push would have been accepted need to be taken into account; any intermediate commits, merges, etc. are no problem (because Jenkins does not build them, and because, once a push fails, the developer will have to add a commit reverting their change and moving it to another file on top, I’m no friend of rewriting).

File matching would be “any files under a certain subdirectory”, nothing fancier than that.

I’ve tried a web search (with two different search engines) for “git prevent pushed files from modification”, but this seems to only show people who want to ignore local changes or somesuch…

I’ve asked in IRC, but with no answer for hours I thought that maybe this was the better place to ask for it.

Thanks in advance, //mirabilos