clarified option -P: allow empty argument;
authorwenzelm
Wed, 05 May 2021 14:17:25 +0200
changeset 73886 f2e836e013cb
parent 73885 a771807df752
child 73887 f17caa5002df
clarified option -P: allow empty argument;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed May 05 14:07:25 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed May 05 14:17:25 2021 +0200
@@ -922,10 +922,7 @@
           context
         }
 
-      build_release(options, context, afp_rev = afp_rev,
-        platform_families =
-          if (platform_families.isEmpty) default_platform_families
-          else platform_families,
+      build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
         more_components = more_components, build_sessions = build_sessions,
         build_library = build_library, parallel_jobs = parallel_jobs, website = website)
     }