changeset 55673:0bf678dd8951

8227613: "draft" header should be in a <header> instead of <div> Reviewed-by: mchung, iris
author jjg
date Fri, 12 Jul 2019 10:44:11 -0700
parents c659942fc471
children ff76baab1c90
files make/Docs.gmk
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/make/Docs.gmk	Fri Jul 12 10:39:19 2019 -0700
+++ b/make/Docs.gmk	Fri Jul 12 10:44:11 2019 -0700
@@ -553,7 +553,7 @@
   $(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.