packaging/deb/postinst

#! /bin/sh

set -i

#install-info --quiet --section "Development" "Development" \
#/usr/doc/dejagnu.info.gz

echo "Edit the master configuration file, /etc/dejagnu/site.exp, if needed"