archive/jdk
1
0
Fork 0
mirror of https://github.com/openjdk/jdk.git synced 2025-09-18 10:04:42 +02:00
Code Issues Projects Releases Packages Wiki Activity Actions

8227613: "draft" header should be in a <header> instead of <div>

Browse source 
Reviewed-by: mchung, iris
This commit is contained in:
Jonathan Gibbons 2019-07-12 10:44:11 -07:00
parent 24b025163b
commit 7821fee0db
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
make/Docs.gmk
View file

@ -553,7 +553,7 @@ $(foreach n, 0 1 2, \
$(eval specs_bottom_rel_path := $(specs_bottom_rel_path)../) \
)
SPECS_TOP := $(if $(filter true, $(IS_DRAFT)), <div class="draft-header">$(DRAFT_TEXT)</div>)
SPECS_TOP := $(if $(filter true, $(IS_DRAFT)), <header class="draft-header">$(DRAFT_TEXT)</header>)
# For all html files in $module/share/specs directories, copy and add the
# copyright footer.