# HG changeset patch # User wenzelm # Date 1736952556 -3600 # Node ID 57b0a02e2774a345f881de88a8deee0cac5cc34d # Parent c551d4a418b9bfe5e0e40904ea3590e99ba83b06 clarified signature: more explicit operations; diff -r c551d4a418b9 -r 57b0a02e2774 src/Pure/library.scala --- a/src/Pure/library.scala Wed Jan 15 15:13:39 2025 +0100 +++ b/src/Pure/library.scala Wed Jan 15 15:49:16 2025 +0100 @@ -147,6 +147,8 @@ def cat_lines(lines: IterableOnce[String]): String = lines.iterator.mkString("\n") + def make_lines(lines: String*): String = cat_lines(lines) + def split_lines(str: String): List[String] = space_explode('\n', str) def prefix_lines(prfx: String, str: String): String = diff -r c551d4a418b9 -r 57b0a02e2774 src/Tools/VSCode/src/component_vscodium.scala --- a/src/Tools/VSCode/src/component_vscodium.scala Wed Jan 15 15:13:39 2025 +0100 +++ b/src/Tools/VSCode/src/component_vscodium.scala Wed Jan 15 15:49:16 2025 +0100 @@ -281,13 +281,13 @@ progress.echo("Prepare ...") Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) { progress.bash( - List( + Library.make_lines( "set -e", platform_info.environment, "./prepare_vscode.sh", // enforce binary diff of code.xpm "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm" - ).mkString("\n"), cwd = build_dir, echo = progress.verbose).check + ), cwd = build_dir, echo = progress.verbose).check Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base, diff_options = "--exclude=.git --exclude=node_modules") }