diff options
| author | Max Weninger | 2012-01-24 13:55:21 +0000 |
|---|---|---|
| committer | Uwe Stieber | 2012-01-24 13:55:21 +0000 |
| commit | fd33ca522d0941e427a4add2c62fba6aef120dfa (patch) | |
| tree | 2fde84076b42f90250957e5cc4bd806a47a6f5e9 /target_explorer/plugins/org.eclipse.tcf.te.ui.terminals.ssh | |
| parent | 6f047bf6a21dcc9be9bf444da123e8b32834da52 (diff) | |
| download | org.eclipse.tcf-fd33ca522d0941e427a4add2c62fba6aef120dfa.tar.gz org.eclipse.tcf-fd33ca522d0941e427a4add2c62fba6aef120dfa.tar.xz org.eclipse.tcf-fd33ca522d0941e427a4add2c62fba6aef120dfa.zip | |
Target Explorer: Use DateFormat.SHORT for terminal tab titles
Diffstat (limited to 'target_explorer/plugins/org.eclipse.tcf.te.ui.terminals.ssh')
| -rw-r--r-- | target_explorer/plugins/org.eclipse.tcf.te.ui.terminals.ssh/src/org/eclipse/tcf/te/ui/terminals/ssh/launcher/SshLauncherDelegate.java | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/target_explorer/plugins/org.eclipse.tcf.te.ui.terminals.ssh/src/org/eclipse/tcf/te/ui/terminals/ssh/launcher/SshLauncherDelegate.java b/target_explorer/plugins/org.eclipse.tcf.te.ui.terminals.ssh/src/org/eclipse/tcf/te/ui/terminals/ssh/launcher/SshLauncherDelegate.java index 6a3dde91c..d16843293 100644 --- a/target_explorer/plugins/org.eclipse.tcf.te.ui.terminals.ssh/src/org/eclipse/tcf/te/ui/terminals/ssh/launcher/SshLauncherDelegate.java +++ b/target_explorer/plugins/org.eclipse.tcf.te.ui.terminals.ssh/src/org/eclipse/tcf/te/ui/terminals/ssh/launcher/SshLauncherDelegate.java @@ -77,7 +77,7 @@ public class SshLauncherDelegate extends AbstractLauncherDelegate { String user = properties.getStringProperty(ITerminalsConnectorConstants.PROP_SSH_USER); if (host != null && user!= null) { - DateFormat format = DateFormat.getDateTimeInstance(DateFormat.LONG, DateFormat.LONG); + DateFormat format = DateFormat.getDateTimeInstance(DateFormat.SHORT, DateFormat.SHORT); String date = format.format(new Date(System.currentTimeMillis())); return NLS.bind(Messages.SshLauncherDelegate_terminalTitle, new String[]{user, host, date}); } |