Added terminal preferences to control which shell & which shell argum…

…ents to use Signed-off-by: Luca Jaeger <[email protected]>
eclipse-theia · Apr 23, 2020 · 4b989d0 · 4b989d0
1 parent 66dd2bc
commit 4b989d0
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 2 deletions.
diff --git a/packages/terminal/src/browser/terminal-preferences.ts b/packages/terminal/src/browser/terminal-preferences.ts
@@ -21,6 +21,14 @@ import { EDITOR_FONT_DEFAULTS } from '@theia/editor/lib/browser';
 export const TerminalConfigSchema: PreferenceSchema = {
     type: 'object',
     properties: {
+        'terminal.shellPath': {
+            type: 'string',
+            description: 'Controls what shell to use',
+        },
+        'terminal.shellArgs': {
+            type: 'array',
+            description: 'Controls what shell arguments to use',
+        },
         'terminal.enableCopy': {
             type: 'boolean',
             description: 'Enable ctrl-c (cmd-c on macOS) to copy selected text',
@@ -111,6 +119,8 @@ export const TerminalConfigSchema: PreferenceSchema = {
 };
 
 export interface TerminalConfiguration {
+    'terminal.shellPath': string
+    'terminal.shellArgs': string
     'terminal.enableCopy': boolean
     'terminal.enablePaste': boolean
     'terminal.integrated.fontFamily': string

diff --git a/packages/terminal/src/browser/terminal-widget-impl.ts b/packages/terminal/src/browser/terminal-widget-impl.ts
@@ -368,8 +368,8 @@ export class TerminalWidgetImpl extends TerminalWidget implements StatefulWidget
         const { cols, rows } = this.term;
 
         const terminalId = await this.shellTerminalServer.create({
-            shell: this.options.shellPath,
-            args: this.options.shellArgs,
+            shell: this.shellPath || this.options.shellPath,
+            args: this.shellArgs || this.options.shellArgs,
             env: this.options.env,
             rootURI,
             cols,
@@ -581,6 +581,14 @@ export class TerminalWidgetImpl extends TerminalWidget implements StatefulWidget
         return this.preferences['terminal.enablePaste'];
     }
 
+    protected get shellPath(): string | undefined {
+        return this.preferences['terminal.shellPath'];
+    }
+
+    protected get shellArgs(): string | undefined {
+        return this.preferences['terminal.shellArgs'];
+    }
+
     protected customKeyHandler(event: KeyboardEvent): boolean {
         const keyBindings = KeyCode.createKeyCode(event).toString();
         const ctrlCmdCopy = (isOSX && keyBindings === 'meta+c') || (!isOSX && keyBindings === 'ctrl+c');