# -*- 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

    # Run gnome-terminal.
    exec \
        gnome-terminal \
        --window \
        --geometry=+100+100 \
        --hide-menubar \
        --disable-factory \
        -e '/bin/bash --norc' \
        "$@"
}