On 6/10/20 2:15 PM, Jonathan Wakely wrote:
And this is another little patch that just avoids running 'git diff' twice, by using tee(1) to write to $GCC_GIT_DIFF_FILE as a side effect of generating the diff to pipe to mklog.py.
Thanks, please install the improvement. Martin