#! /bin/bash # Last edited on 2024-03-27 10:11:13 by stolfi cmd=${0##*/} usage="${cmd} {DIFFARGS ...} " # Runs {diff} and pipes the output through {prettify-diff-output}. diff "$@" | prettify_diff_output.sh