#! /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"