# -*- shell-script -*-

# Place any local environment variables required in 'local'.
if [ -f local ]; then source local; fi

export PS1="$ "

export HISTFILE=$talkdir/history

rm -f $HISTFILE
touch $HISTFILE

add_history ()
{
    echo "$@" >> $HISTFILE
}

terminal ()
{
    # Make $HISTFILE unwritable so the shell won't update it
    # when it exits.
    chmod -w $HISTFILE

    # Execute a shell.
    bash --norc "$@"
}
