On Sat, Feb 02, 2002 at 06:22:08PM +0000, Pete Ryland wrote:
> function set_title() {
> if [ x$1 != x--keep ]; then
> SET_TITLE_EXTRA="$@"
> fi
> if [ -z "$SET_TITLE_EXTRA" ]; then
> NAME="$USER@$HOSTNAME:$PWD"
> else
> NAME="$USER@$HOSTNAME:$PWD ($SET_TITLE_EXTRA)"
> fi
> echo -n
> }
Hmm.. that echo -n should obviously be echo -n <esc>]\;$NAME<^g>
where <esc> and <^g> are the appropriate chars.
Pete