# HG changeset patch
# User wenzelm
# Date 1620217045 -7200
# Node ID f2e836e013cbdafaf283100db7dec7753ad3657d
# Parent  a771807df7520a697d4ebf825c005de99fd46c4e
clarified option -P: allow empty argument;

diff -r a771807df752 -r f2e836e013cb 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)
     }