[hcoop/zz_old/debian/smlnj.git] / debian / deregister

#!/bin/sh

set -e

if [ $# -ne 1 ] ; then
    echo "usage: deregister name"
    exit 1
fi

name=$1

sed -i -e "/^$name /d" /usr/lib/smlnj/lib/pathconfig
Commit	Line	Data
4dd335d4 JM	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