mathieui 48e59d377f Fix #2282 (change the terminal title depending on the tab name) ... - change_title plugin		2014-04-30 21:55:19 +02:00
..
source	Fix #2282 (change the terminal title depending on the tab name)	2014-04-30 21:55:19 +02:00
stub
Makefile