#!/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