debian/deregister

   1 #!/bin/sh
   2
   3 set -e
   4
   5 if [ $# -ne 1 ] ; then
   6     echo "usage: deregister name"
   7     exit 1
   8 fi
   9
  10 name=$1
  11
  12 sed -i -e "/^$name /d" /usr/lib/smlnj/lib/pathconfig