diff options
| author | Mike Krüger <mkrueger@xamarin.com> | 2012-11-27 10:46:41 +0400 |
|---|---|---|
| committer | Mike Krüger <mkrueger@xamarin.com> | 2012-11-27 10:46:41 +0400 |
| commit | 333b27bec79bc474c63d3c7e78c4931a61ab566d (patch) | |
| tree | 77de45e202e94dbe887928a448cfe47d461c85f0 /main/src/addins/GnomePlatform | |
| parent | 8c7404e58abbf17f310f496a65baee6aaf9d322c (diff) | |
Fixed 'Bug 8594 - [ui-refresh] Debuggin on Linux is broken.'.
Diffstat (limited to 'main/src/addins/GnomePlatform')
| -rw-r--r-- | main/src/addins/GnomePlatform/GnomePlatform.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/main/src/addins/GnomePlatform/GnomePlatform.cs b/main/src/addins/GnomePlatform/GnomePlatform.cs index 4e4ed2dfec..7c2a09cd10 100644 --- a/main/src/addins/GnomePlatform/GnomePlatform.cs +++ b/main/src/addins/GnomePlatform/GnomePlatform.cs @@ -285,6 +285,10 @@ namespace MonoDevelop.Platform preferred_terminal = "gnome-terminal"; preferred_runner = GnomeTerminalRunner; } + else if (!String.IsNullOrEmpty (Environment.GetEnvironmentVariable ("MATE_DESKTOP_SESSION_ID"))) { + preferred_terminal = "mate-terminal"; + preferred_runner = GnomeTerminalRunner; + } else { preferred_terminal = fallback_terminal; preferred_runner = fallback_runner; |