src/Tools/Setup/src/Build.java
changeset 74059 55505e7bbfb3
parent 74058 4b15a1e25537
child 74061 203dfa8bc0fc
--- a/src/Tools/Setup/src/Build.java	Sat Jul 24 17:06:50 2021 +0200
+++ b/src/Tools/Setup/src/Build.java	Sat Jul 24 18:01:24 2021 +0200
@@ -50,6 +50,8 @@
 
     public static String BUILD_PROPS = "build.props";
     public static String COMPONENT_BUILD_PROPS = "etc/build.props";
+
+    public static String TITLE = "title";
     public static String MODULE = "module";
     public static String NO_BUILD = "no_build";
 
@@ -119,12 +121,7 @@
             }
         }
 
-        public String title() {
-            String title = _props.getProperty("title", "");
-            if (title.isEmpty()) { throw new RuntimeException(error_message("Missing title")); }
-            else return title;
-        }
-
+        public String title() { return _props.getProperty(TITLE, ""); }
 
         public String module_name() { return _props.getProperty(MODULE, ""); }
         public String module_result() { return get_bool(NO_BUILD) ? "" : module_name(); }
@@ -487,7 +484,9 @@
                     shasum = _shasum.toString();
                 }
                 if (fresh || !shasum_old.equals(shasum)) {
-                    System.out.print("### Building " + title + " (" + jar_path + ") ...\n");
+                    if (!title.isEmpty()) {
+                        System.out.print("### Building " + title + " (" + jar_path + ") ...\n");
+                    }
 
                     String isabelle_classpath = Environment.getenv("ISABELLE_CLASSPATH");