# HG changeset patch
# User wenzelm
# Date 1736945122 -3600
# Node ID ef849800cc97aa4c2281bd9c9a2a9e18ac0e2786
# Parent  7a858ff1c978f88db3d89a8b75427ee2271e20bd
clarified signature: more explicit operations;

diff -r 7a858ff1c978 -r ef849800cc97 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Jan 14 11:34:17 2025 +0100
+++ b/src/Pure/System/isabelle_system.scala	Wed Jan 15 13:45:22 2025 +0100
@@ -503,6 +503,18 @@
     }
   }
 
+  def git_clone(url: String, target: Path,
+    checkout: String = "HEAD",
+    ssh: SSH.System = SSH.Local,
+    progress: Progress = new Progress
+  ): Unit = {
+    progress.echo("Cloning " + quote(url))
+    bash(
+      "git clone --quiet --no-checkout " + Bash.string(url) + " . && " +
+      "git checkout --quiet --detach " + Bash.string(checkout),
+      ssh = ssh, cwd = ssh.make_directory(target)).check
+  }
+
   def open(arg: String): Unit =
     bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
 
diff -r 7a858ff1c978 -r ef849800cc97 src/Tools/VSCode/src/component_vscodium.scala
--- a/src/Tools/VSCode/src/component_vscodium.scala	Tue Jan 14 11:34:17 2025 +0100
+++ b/src/Tools/VSCode/src/component_vscodium.scala	Wed Jan 15 13:45:22 2025 +0100
@@ -81,12 +81,7 @@
 
     def get_vscodium_repository(build_dir: Path, progress: Progress = new Progress): Unit = {
       progress.echo("Getting VSCodium repository ...")
-      Isabelle_System.bash(
-        List(
-          "set -e",
-          "git clone -n " + Bash.string(vscodium_repository) + " .",
-          "git checkout -q " + Bash.string(version)
-        ).mkString("\n"), cwd = build_dir).check
+      Isabelle_System.git_clone(vscodium_repository, build_dir, checkout = version)
 
       progress.echo("Getting VSCode repository ...")
       Isabelle_System.bash(environment + "\n" + "./get_repo.sh", cwd = build_dir).check