# -*- 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 "$@" }