Feature request: Rename tab
In the old times gnome-terminal had Rename Tab in the Tabs' menu. For the past couple of years, it has gone. I wish we could get it back again.
Usually I work with large number of tabs in parallel and the current labels are not informative enough. Commanding the label change via PS1 is not convinient, especially if I am logged to a remote computer.