Hi Trevor,

Looks like my fear about "other terminal types" was not unfounded after
all: gnome-terminal uses a terminal type of 1 and that leads to problems
(see http://debbugs.gnu.org/16988 for the discussion).

I'm leaning towards the conservative option of replacing your "[0-9]+"
with "0\\|41", WDYT?


        Stefan