6
if [ "$1" = "configure" ]; then
7
## install-info --quiet --section "Development" "Development" \
8
## /usr/share/info/dejagnu.info.gz
9
if command -v install-docs > /dev/null 2>&1; then
10
install-docs -i /usr/share/doc-base/dejagnu
14
echo "Edit the master configuration file, /etc/dejagnu/site.exp, if needed"