![[Jenkins]](/jenkins/static/51af4dc4/images/svgs/logo.svg){kind=logo}
Summary
- clarified signature: tree structure is not essential;
| The file was modified | Admin/jenkins/build/ci_build_benchmark.scala (diff) |
| The file was modified | Admin/jenkins/build/ci_build_makeall.scala (diff) |
| The file was modified | Admin/jenkins/build/ci_build_makeall_seq.scala (diff) |
| The file was modified | src/Pure/Admin/ci_profile.scala (diff) |
| The file was modified | src/Pure/System/isabelle_process.scala (diff) |
| The file was modified | src/Pure/Thy/sessions.scala (diff) |
| The file was modified | src/Pure/Tools/build.scala (diff) |
| The file was modified | src/Pure/Tools/ml_process.scala (diff) |