#!/bin/sh

# Remove INFOCOM_PATH from /etc/profile
# If it has been changed, /etc/profile may be left in an odd state
mv /etc/profile /etc/profile.old
sed 's%export INFOCOM_PATH=/usr/local/games/infocom:/usr/local/games/inform%%' </etc/profile.old >/etc/profile
rm -f /etc/profile.old
