# HG changeset patch # User wenzelm # Date 1475602998 -7200 # Node ID 44b6c620c371378998a0114b524da80edd209807 # Parent 6957bd29a950e6e809083505efb518cdecf97d34 more thorought update of components; diff -r 6957bd29a950 -r 44b6c620c371 src/Pure/Tools/build_history.scala --- a/src/Pure/Tools/build_history.scala Tue Oct 04 19:38:43 2016 +0200 +++ b/src/Pure/Tools/build_history.scala Tue Oct 04 19:43:18 2016 +0200 @@ -109,6 +109,9 @@ File.append(etc_settings, "\n" + Library.terminate_lines(component_settings)) + isabelle("components -a", redirect = true, echo = verbose).check + + /* augmented settings */ val ml_settings = @@ -169,9 +172,11 @@ File.append(etc_settings, "\n" + Library.terminate_lines(more_settings)) + isabelle("components -a", redirect = true, echo = verbose).check + + /* build */ - isabelle("components -a", redirect = true, echo = verbose).check isabelle("jedit -b" + (if (fresh) " -f" else ""), redirect = true, echo = verbose).check isabelle("build " + File.bash_args(build_args), redirect = true, echo = verbose)