dot/shell-rc: Colourize `diff' output similarly to `grep'.
authorMark Wooding <mdw@distorted.org.uk>
Fri, 2 Aug 2019 19:38:05 +0000 (20:38 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Sat, 3 Aug 2019 02:14:21 +0000 (03:14 +0100)
commit049cd0157dcb6204cc0f90b7c54dd1b10de34566
treeb351151ee1162a102fc807b716190830d24a4cbe
parentb59e8644263f6e5bd31778ffada9be6e0a539a92
dot/shell-rc: Colourize `diff' output similarly to `grep'.

There's a problem here because of a `zsh' bug:

$ diff -u <(thing) <(thong) | blah
diff: /proc/self/fd/13: No such file or directory
diff: /proc/self/fd/14: No such file or directory

caused by the process-substitution pipes being lost somewhere.

Work around this as (a)

$ diff -u =(thing) =(thong) | blah

(produces temporary files), or (b)

$ { diff -u <(thing) <(thong) } | blah

(extra typing).
dot/shell-rc