# HG changeset patch # User wenzelm # Date 1674576960 -3600 # Node ID 973de7855948c9e436ccf8e24c95ed61338e4b25 # Parent 2515198c55e45ae37d3ddc705cfb0ebe3795c89e removed unused user_home argument (see also 897f1ac84aab and 19b6091c2137); diff -r 2515198c55e4 -r 973de7855948 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Tue Jan 24 16:08:28 2023 +0100 +++ b/src/Pure/Admin/build_history.scala Tue Jan 24 17:16:00 2023 +0100 @@ -91,7 +91,6 @@ /** local build **/ - private val default_user_home = Path.USER_HOME private val default_multicore = (1, 1) private val default_heap = 1500 private val default_isabelle_identifier = "build_history" @@ -99,7 +98,6 @@ def local_build( options: Options, root: Path, - user_home: Path = default_user_home, progress: Progress = new Progress, afp: Boolean = false, afp_partition: Int = 0, @@ -176,8 +174,7 @@ /* main */ val other_isabelle = - Other_Isabelle(root, isabelle_identifier = isabelle_identifier, - user_home = user_home, progress = progress) + Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = progress) val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname() val build_history_date = Date.now() @@ -247,7 +244,7 @@ val build_result = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, - user_home = user_home, progress = build_out_progress) + progress = build_out_progress) .bash("bin/isabelle build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true, strict = false) @@ -413,7 +410,6 @@ var output_file = "" var ml_statistics_step = 1 var build_tags = List.empty[String] - var user_home = default_user_home var verbose = false var exit_code = false @@ -443,7 +439,6 @@ -p TEXT additional text for generated etc/preferences -s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1) -t TAG free-form build tag (multiple occurrences possible) - -u DIR alternative USER_HOME directory -v verbose -x return overall exit code from build processes @@ -476,7 +471,6 @@ "p:" -> (arg => more_preferences = more_preferences ::: List(arg)), "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)), "t:" -> (arg => build_tags = build_tags ::: List(arg)), - "u:" -> (arg => user_home = Path.explode(arg)), "v" -> (_ => verbose = true), "x" -> (_ => exit_code = true)) @@ -490,7 +484,7 @@ val progress = new Console_Progress(stderr = true) val results = - local_build(Options.init(), root, user_home = user_home, progress = progress, + local_build(Options.init(), root, progress = progress, afp = afp, afp_partition = afp_partition, isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step, component_repository = component_repository, components_base = components_base, diff -r 2515198c55e4 -r 973de7855948 src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Tue Jan 24 16:08:28 2023 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Tue Jan 24 17:16:00 2023 +0100 @@ -11,17 +11,15 @@ def apply( isabelle_home: Path, isabelle_identifier: String = "", - user_home: Path = Path.USER_HOME, progress: Progress = new Progress ): Other_Isabelle = { - new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress) + new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, progress) } } final class Other_Isabelle private( val isabelle_home: Path, val isabelle_identifier: String, - user_home: Path, progress: Progress ) { override def toString: String = isabelle_home.toString @@ -40,7 +38,7 @@ strict: Boolean = true ): Process_Result = { progress.bash( - "export USER_HOME=" + File.bash_path(user_home) + "\n" + + "export USER_HOME=" + File.bash_path(Path.USER_HOME) + "\n" + Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script, env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict) }