jdk/makefiles/GendataHtml32dtd.gmk
changeset 14231 a0c23c1c010f
parent 13164 72c5d01a857d
child 20547 453837141fac
--- a/jdk/makefiles/GendataHtml32dtd.gmk	Wed Jul 05 18:26:51 2017 +0200
+++ b/jdk/makefiles/GendataHtml32dtd.gmk	Fri Oct 26 14:23:29 2012 -0700
@@ -30,6 +30,6 @@
 	$(ECHO) "Generating HTML DTD file"
 	$(MKDIR) -p $(@D)
 	$(RM) $@
-	($(TOOL_DTDBUILDER) html32 > $@) || exit 1
+	($(TOOL_DTDBUILDER) $(LOG_INFO) html32 > $@) || exit 1
 
-GENDATA_HTML32DTD += $(HTML32DTD)
\ No newline at end of file
+GENDATA_HTML32DTD += $(HTML32DTD)