diff options
Diffstat (limited to 'src/ide.js')
-rw-r--r-- | src/ide.js | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -36,9 +36,9 @@ UnknownModuleError.prototype.constructor = UnknownModuleError; | |||
36 | module.exports.UnknownModuleError = UnknownModuleError; | 36 | module.exports.UnknownModuleError = UnknownModuleError; |
37 | 37 | ||
38 | function spawnIdeClient(body, options) { | 38 | function spawnIdeClient(body, options) { |
39 | const ideClientCommand = 'purs'; | 39 | const ideClientCommand = options.pscIdeClient || 'purs'; |
40 | 40 | ||
41 | const ideClientArgs = ['ide', 'client'].concat(dargs(options.pscIdeArgs)); | 41 | const ideClientArgs = (options.pscIdeClient ? [] : ['ide', 'client']).concat(dargs(options.pscIdeClientArgs)); |
42 | 42 | ||
43 | const stderr = []; | 43 | const stderr = []; |
44 | 44 | ||
@@ -144,9 +144,9 @@ function formatIdeResult(result, options, index, length) { | |||
144 | module.exports.connect = function connect(psModule) { | 144 | module.exports.connect = function connect(psModule) { |
145 | const options = psModule.options | 145 | const options = psModule.options |
146 | 146 | ||
147 | const serverCommand = 'purs'; | 147 | const serverCommand = options.pscIdeServer || 'purs'; |
148 | 148 | ||
149 | const serverArgs = ['ide', 'server'].concat(dargs(Object.assign({ | 149 | const serverArgs = (options.pscIdeServer ? [] : ['ide', 'server']).concat(dargs(Object.assign({ |
150 | outputDirectory: options.output, | 150 | outputDirectory: options.output, |
151 | '_': options.src | 151 | '_': options.src |
152 | }, options.pscIdeServerArgs))); | 152 | }, options.pscIdeServerArgs))); |