--- a/src/Pure/Admin/build_history.scala Tue May 16 15:53:27 2017 +0200
+++ b/src/Pure/Admin/build_history.scala Tue May 16 16:04:50 2017 +0200
@@ -29,7 +29,6 @@
arch_64: Boolean,
heap: Int,
max_heap: Option[Int],
- init_settings: List[String],
more_settings: List[String]): String =
{
val (ml_platform, ml_settings) =
@@ -85,7 +84,6 @@
"ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
val settings =
- (if (init_settings.isEmpty) Nil else List(init_settings)) :::
List(ml_settings, thread_settings) :::
(if (more_settings.isEmpty) Nil else List(more_settings))
@@ -163,11 +161,10 @@
{
/* init settings */
- other_isabelle.init_settings(components_base, nonfree)
+ other_isabelle.init_settings(components_base, nonfree, init_settings)
other_isabelle.resolve_components(verbose)
val ml_platform =
- augment_settings(other_isabelle, threads, arch_64, heap, max_heap,
- init_settings, more_settings)
+ augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
val isabelle_output_log = isabelle_output + Path.explode("log")
--- a/src/Pure/Admin/other_isabelle.scala Tue May 16 15:53:27 2017 +0200
+++ b/src/Pure/Admin/other_isabelle.scala Tue May 16 16:04:50 2017 +0200
@@ -33,7 +33,7 @@
/* init settings */
- def init_settings(components_base: String, nonfree: Boolean)
+ def init_settings(components_base: String, nonfree: Boolean, more_settings: List[String])
{
if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
error("Cannot proceed with existing user settings file: " + etc_settings)
@@ -56,6 +56,11 @@
"init_components " + File.bash_path(components_base_path) +
" \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
}
- File.append(etc_settings, "\n" + terminate_lines(component_settings))
+
+ val settings =
+ List(component_settings) :::
+ (if (more_settings.isEmpty) Nil else List(more_settings))
+
+ File.append(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
}
}