#! /bin/csh -f
# Last modified on Mon Oct 20 23:41:08 1986     by stolfi
# A less verbose form of directory diff:
diff $* | sed '/^[-<>0-9]/d'