changeset 77218 | 86217697863c |
parent 77084 | f9a858060836 |
child 77369 | df17355f1e2c |
--- a/src/Pure/Tools/dotnet_setup.scala Mon Feb 06 16:26:40 2023 +0100 +++ b/src/Pure/Tools/dotnet_setup.scala Mon Feb 06 16:29:19 2023 +0100 @@ -186,7 +186,7 @@ "V:" -> (arg => version = arg), "f" -> (_ => force = true), "n" -> (_ => dry_run = true), - "p:" -> (arg => platforms = Library.space_explode(',', arg).map(check_platform_spec)), + "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)), "v" -> (_ => verbose = true)) val more_args = getopts(args)