summaryrefslogtreecommitdiff
path: root/debian/prerm
diff options
context:
space:
mode:
authorMarcus Brinkmann <marcus@gnu.org>2001-10-04 02:35:28 +0000
committerMarcus Brinkmann <marcus@gnu.org>2001-10-04 02:35:28 +0000
commit21ea10295a2b95b5b89ee0097aabde64ce01317c (patch)
treed505d53a5e225a5fbde172af588c190d2dd51aa0 /debian/prerm
parent5df48e5543060daf29f59b910c567d74205da9d6 (diff)
2001-10-04 Marcus Brinkmann <marcus@gnu.org>
* doc: New directory. * doc/Makefile.in: New file. * doc/gpl.texi: Likewise. * doc/fdl.texi: Likewise. * doc/mach.texi: Likewise. * configure.in: Add doc/Makefile to AC_OUTPUT call. * configure: Regenerated. * Makefile.in (dist): Create directories doc and debian. (doc-files): New variable with documentation files. (debian-files): New variable with Debian packaging files. * debian/rules (stamp-build): Build documentation. (build-gnumach): Install the documentation into the gnumach package. * debian/postrm: New file to install info document. * debian/prerm: New file to install info document.
Diffstat (limited to 'debian/prerm')
-rw-r--r--debian/prerm3
1 files changed, 3 insertions, 0 deletions
diff --git a/debian/prerm b/debian/prerm
new file mode 100644
index 0000000..b033806
--- /dev/null
+++ b/debian/prerm
@@ -0,0 +1,3 @@
+#!/bin/sh -e
+
+install-info --quiet --remove /usr/share/info/mach.info