# 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