> And maybe even more interestnig -- is there a point to this whole > make_diff directory at all in these days of git? Or should we just > remove it rather than try to fix it?
There's also src/tools/make_mkid which use this mkid tool. +1 for removing. If anything, it seems better replaced by extended documentation on the existing wiki article [0] on how to use "git format-patch".
