Dear Julien,

now I generated the diff by ~git diff > configfile.diff-patch~ and tested
it on commit ~a582d863465990642d331bc05bf073f47fb80908~ by
~git apply configfile.diff-patch~. I hope you can apply it now, even on an
updated origin.

Kind regards,
Stefan