#!/bin/sh

#   May 27/97 - F.Majaess

#id drain_input - script used to get rid of piped input when running
#                 in the background.

set -e
# cat > /dev/null 2> /dev/null
cat > /dev/null 
exit