diff options
author | Omar Vega Ramos <ovruni@gnu.org.pe> | 2015-07-07 17:04:44 -0500 |
---|---|---|
committer | Omar Vega Ramos <ovruni@gnu.org.pe> | 2015-07-07 17:04:44 -0500 |
commit | a83ef5efe6adc5d6d4492fbe6421b34aa2e0ebb6 (patch) | |
tree | 03f6cafcc29fbccbbb166fdffed89a956e4575a9 /pcr/wdiff/wdiff.install | |
parent | 2d8d34c87fff47ed554f5c972d2e768c8b165906 (diff) |
wdiff-1.2.2-1: updating version
Diffstat (limited to 'pcr/wdiff/wdiff.install')
-rw-r--r-- | pcr/wdiff/wdiff.install | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/pcr/wdiff/wdiff.install b/pcr/wdiff/wdiff.install new file mode 100644 index 000000000..40c5b92fc --- /dev/null +++ b/pcr/wdiff/wdiff.install @@ -0,0 +1,13 @@ +infodir=/usr/share/info + +post_install() { + install-info $infodir/wdiff.info $infodir/dir 2> /dev/null +} + +post_upgrade() { + post_install $1 +} + +pre_remove() { + install-info --delete $infodir/wdiff.info $infodir/dir 2> /dev/null +} |