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
stub
Makefile	Beginning of the migration to reST documentation	2013-04-08 18:52:35 +02:00