| #
59e8b99e |
|
26-Jun-2018 |
Lars Hupel <lars.hupel@mytum.de> |
support NUMA shuffling in CI
|
| #
1ec4d40f |
|
20-Apr-2018 |
wenzelm <none@none> |
workaround for jdk-10.0.1;
|
| #
5a0e9b6e |
|
07-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
| #
e8540ef6 |
|
07-Apr-2017 |
wenzelm <none@none> |
explicit Sessions.Selection;
|
| #
80237638 |
|
06-Apr-2017 |
wenzelm <none@none> |
clarified signature: tree structure is not essential;
|
| #
33b957d3 |
|
26-Feb-2017 |
wenzelm <none@none> |
clarified defaults;
|
| #
5195252e |
|
18-Oct-2016 |
Lars Hupel <lars.hupel@mytum.de> |
Jenkins: build in system mode again
(backout of 3dbfd6758735)
|
| #
293cbdb4 |
|
18-Oct-2016 |
Lars Hupel <lars.hupel@mytum.de> |
Jenkins: configurable clean build
|
| #
f456991b |
|
15-Oct-2016 |
wenzelm <none@none> |
clarified hg.id operation, with explicit tip as default;
|
| #
b43a58e0 |
|
15-Oct-2016 |
Lars Hupel <lars.hupel@mytum.de> |
Jenkins: don't build in system mode
|
| #
24fe27ba |
|
12-Oct-2016 |
wenzelm <none@none> |
modernized;
|
| #
7768c0d1 |
|
12-Oct-2016 |
wenzelm <none@none> |
clarified files;
--HG--
rename : src/Pure/Tools/build_history.scala => src/Pure/Admin/build_history.scala
rename : src/Pure/Tools/build_log.scala => src/Pure/Admin/build_log.scala
rename : src/Pure/Tools/ci_api.scala => src/Pure/Admin/ci_api.scala
rename : src/Pure/Tools/ci_profile.scala => src/Pure/Admin/ci_profile.scala
|