git: configure patdiff through [patdiff] git section (#6978)

This adds the ability to enable the patdiff program as git differ.
Website of the project: https://opensource.janestreet.com/patdiff/
This commit is contained in:
Plume 2025-05-08 15:15:51 +02:00 committed by GitHub
parent 50894120e8
commit 2ede089d11
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 68 additions and 1 deletions

View file

@ -9,4 +9,5 @@
git-without-signing = ./git-without-signing.nix;
git-with-hooks = ./git-with-hooks.nix;
git-with-maintenance = ./git-with-maintenance.nix;
git-patdiff = ./git-patdiff.nix;
}