changeset 78178 | a177f71dc79f |
parent 77414 | 0d5994eef9e6 |
--- a/src/Pure/ML/ml_console.scala Mon Jun 19 22:28:09 2023 +0200 +++ b/src/Pure/ML/ml_console.scala Tue Jun 20 14:25:06 2023 +0200 @@ -48,7 +48,7 @@ if (more_args.nonEmpty) getopts.usage() - val store = Sessions.store(options) + val store = Store(options) // build logic if (!no_build && !raw_ml_system) {