tuned signature;
authorwenzelm
Wed, 02 Mar 2022 21:14:09 +0100
changeset 75189 f304a2a5080f
parent 75188 f2b93941ee43
child 75190 fa9ca4563d72
tuned signature;
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 02 20:37:46 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Mar 02 21:14:09 2022 +0100
@@ -35,7 +35,7 @@
 
     const server_options: ServerOptions =
       platform.is_windows() ?
-        { command: library.cygwin_root() + "\\bin\\bash",
+        { command: library.cygwin_bash(),
           args: ["-l", isabelle_tool, "vscode_server"].concat(isabelle_args) } :
         { command: isabelle_tool,
           args: ["vscode_server"].concat(isabelle_args) }
--- a/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 20:37:46 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 21:14:09 2022 +0100
@@ -51,7 +51,7 @@
 }
 
 
-/* system path representations */
+/* Windows/Cygwin */
 
 export function cygwin_root(): string
 {
@@ -61,6 +61,14 @@
   else { return "" }
 }
 
+export function cygwin_bash(): string
+{
+  return cygwin_root() + "\\bin\\bash"
+}
+
+
+/* system path representations */
+
 function slashes(s: string): string
 {
   return s.replace(/\\/g, "/")