From 4c49a936c409a23100e8c0caa706d6f21d67ed69 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Sat, 5 Mar 2022 00:12:08 +0000 Subject: [PATCH] PHP: fix some tag soup issues Use the existing template's support for headers, don't nest HTML tags. --- rules/generate.rb | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/rules/generate.rb b/rules/generate.rb index 5bba466..2626ecd 100755 --- a/rules/generate.rb +++ b/rules/generate.rb @@ -302,10 +302,10 @@ def write_tex(file, fin) PHP_HEADER = < - - -Capture the Flag with Stuff + + +HEAD; - - - - EOH # Only used for testing; the PHP header is normally used.