RE: Disk Space on /usr/dcs/projects

Thanks for the warning! I checked and the executables take up about 2/3 of
the space (380MB) vs. about 180MB for the libs. Since we are usually only
debugging one executable at a time (if any), I modified Makefile.common to
strip each executable in tools/Debug by default. You can define
KEEP_SYMBOLS in the Makefile of any particular tool in order to avoid
stripping that executable.

I have added KEEP_SYMBOLS = 1 in the Makefile for opt since that is likely
to be needed by most people. It is undefined for all other executables.

This saves about 300MB per user!