← Back to branch summary

~ubuntu-branches/ubuntu/trusty/dejagnu/trusty-updates 

1
2
3
4
5
6
7
8
9
10

#! /bin/sh

set -e

if [ "$1" = "upgrade" -o "$1" = "remove" ]; then
##    install-info --quiet --remove dejagnu
    if command -v install-docs > /dev/null 2>&1; then
	install-docs -r dejagnu || true
    fi
fi