changeset 72076 | bd9d1ce274c9 |
parent 72022 | 45865bb06182 |
child 72103 | 7b318273a4aa |
--- a/src/Pure/Tools/build.scala Sun Jul 26 21:53:29 2020 +0200 +++ b/src/Pure/Tools/build.scala Sun Jul 26 22:28:43 2020 +0200 @@ -216,7 +216,7 @@ } else Nil - if (options.bool("pide_session")) { + if (options.bool("pide_session") || true /* FIXME test */) { val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) {