# HG changeset patch
# User erikj
# Date 1525106948 25200
# Node ID ae58e24ce81a1ed965dbe42cb58a02b790616441
# Parent  891132345d430850ad4e80969306811814947146
8202383: Custom extensions for jvmti doc
Reviewed-by: erikj
Contributed-by: archana.nogriya@uk.ibm.com

diff -r 891132345d43 -r ae58e24ce81a make/Docs.gmk
--- a/make/Docs.gmk	Mon Apr 30 09:37:10 2018 -0700
+++ b/make/Docs.gmk	Mon Apr 30 09:49:08 2018 -0700
@@ -561,7 +561,7 @@
 JDK_SPECS_TARGETS += $(COPY_JDWP_PROTOCOL)
 
 # Get jvmti.html from the main jvm variant (all variants' jvmti.html are identical).
-JVMTI_HTML := $(HOTSPOT_OUTPUTDIR)/variant-$(JVM_VARIANT_MAIN)/gensrc/jvmtifiles/jvmti.html
+JVMTI_HTML ?= $(HOTSPOT_OUTPUTDIR)/variant-$(JVM_VARIANT_MAIN)/gensrc/jvmtifiles/jvmti.html
 $(eval $(call SetupCopyFiles, COPY_JVMTI_HTML, \
     FILES := $(JVMTI_HTML), \
     DEST := $(DOCS_OUTPUTDIR)/specs, \