src/Pure/ML/ml_console.scala
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) {