[dist] Remove old git cop config option
got removed in d092bb05edb1ddd048025bc092ccf2275af4facd. Fixes PR#4534.
parent
07b488e8
Please register or sign in to comment
got removed in d092bb05edb1ddd048025bc092ccf2275af4facd. Fixes PR#4534.