]> git.openstreetmap.org Git - chef.git/commitdiff
Try diff merging several times at five minute intervals
authorTom Hughes <tom@compton.nu>
Tue, 16 May 2017 07:52:02 +0000 (08:52 +0100)
committerTom Hughes <tom@compton.nu>
Tue, 16 May 2017 07:52:02 +0000 (08:52 +0100)
This way if the underlying diffs are ready yet we will have another
go later, and extra ones are harmless as they do nothing.


No differences found