author | wenzelm |
Sun, 26 Jul 2020 22:28:43 +0200 | |
changeset 72076 | bd9d1ce274c9 |
parent 72075 | 9c0b835d4cc2 |
child 72077 | 1d6c3cba47fe |
--- 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) {