# puts a specific textual label on the terminal title bar.
# this doesn't consider any previous titles; it just labels the terminal.
# puts a specific textual label on the terminal title bar.
# this doesn't consider any previous titles; it just labels the terminal.
echo -n -e "\033]0;${title}\007"
else
# not running interactively, so just echo the title.
echo -n -e "\033]0;${title}\007"
else
# not running interactively, so just echo the title.
- # we're enforcing a new title from here on.
- unset PRIOR_TERMINAL_TITLE
+
+#tricky tries to get it to be available when we ask for it in get_terminal_title
+ sync
+# echo -n
+
+# # we're enforcing a new title from here on.
+# unset PRIOR_TERMINAL_TITLE
save_terminal_title
}
# echoes back the current title on the terminal window, if we can acquire it.
function get_terminal_title()
{
save_terminal_title
}
# echoes back the current title on the terminal window, if we can acquire it.
function get_terminal_title()
{
}
# reads the current terminal title, if possible, and saves it to our record.
function save_terminal_title()
{
local title="$(get_terminal_title)"
}
# reads the current terminal title, if possible, and saves it to our record.
function save_terminal_title()
{
local title="$(get_terminal_title)"
# there was a title, so save it.
if [ ! -z "$DEBUG_TERM_TITLE" ]; then
# there was a title, so save it.
if [ ! -z "$DEBUG_TERM_TITLE" ]; then
else
# the terminal had no title, or we couldn't access it, or there's no terminal.
if [ ! -z "$DEBUG_TERM_TITLE" ]; then
else
# the terminal had no title, or we couldn't access it, or there's no terminal.
if [ ! -z "$DEBUG_TERM_TITLE" ]; then