#!/bin/sh
# Here is a generic "wrapper" around the "make" command.  This script
# runs make in the background and sends all its output to "Make.out".
# A message is written to stdout when it finished. I usually run this
# in the background, and edit the Make.out file when it finishes.

#if [ ! -n "$CFLAGS" ];then CFLAGS='-DPOSIX'; fi
#nice make CFLAGS="$CFLAGS" $* >Make.out 2>&1

nice make $* >Make.out 2>&1 | grep --exclude 'middle=d' | grep --exclude deprecated

echo `pwd` Make "$*" done.