# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1718219681 -7200
# Node ID 42dafe6efb8d73e6211099cff8d80316ca73c514
# Parent  4fa6e5f9d3939d98679f69392228ce59ed3d8c89
vscode: indent;

diff -r 4fa6e5f9d393 -r 42dafe6efb8d src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Wed Jun 12 21:22:01 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_main.scala	Wed Jun 12 21:14:41 2024 +0200
@@ -32,7 +32,7 @@
     verbose: Boolean = false,
     background: Boolean = false,
     progress: Progress = new Progress
-): Process_Result = {
+  ): Process_Result = {
     def platform_path(s: String): String = File.platform_path(Path.explode(s))
 
     val args_json =