diff options
Diffstat (limited to 'debian/coq.postinst')
-rwxr-xr-x | debian/coq.postinst | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/debian/coq.postinst b/debian/coq.postinst deleted file mode 100755 index 5d567619..00000000 --- a/debian/coq.postinst +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/sh - -set -e - -TEXCONFIG=/usr/bin/mktexlsr - -case "$1" in - configure) - if [ -e $TEXCONFIG ] - then - $TEXCONFIG - fi - ;; - - abort-upgrade|abort-remove|abort-deconfigure) - ;; - - *) - echo "postinst called with unknown argument \`$1'" >&2 - exit 0 - ;; -esac - -#DEBHELPER# - -exit 0 |