src/Pure/Admin/build_release.scala
changeset 66923 914935f8a462
parent 66910 20d61ffa9867
child 67045 6c94f749410a
--- a/src/Pure/Admin/build_release.scala	Thu Oct 26 23:31:03 2017 +0200
+++ b/src/Pure/Admin/build_release.scala	Fri Oct 27 11:46:03 2017 +0200
@@ -223,7 +223,7 @@
         "W:" -> (arg => website = Some(Path.explode(arg))),
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
         "l" -> (_ => build_library = true),
-        "p:" -> (arg => platform_families = Library.space_explode(',', arg)),
+        "p:" -> (arg => platform_families = space_explode(',', arg)),
         "r:" -> (arg => rev = arg))
 
       val more_args = getopts(args)