From 7d6511799e6a4c1a127b217fc8f2e85e8725d15d Mon Sep 17 00:00:00 2001 From: Mike Gerwitz Date: Mon, 26 Oct 2015 23:54:51 -0400 Subject: [PATCH] Correct webdoc manual styling for Texinfo 5.2 --- tools/webdoc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/webdoc b/tools/webdoc index 5997c61..14feac0 100755 --- a/tools/webdoc +++ b/tools/webdoc @@ -83,8 +83,8 @@ webify() s##\n&#; ' "$docpath" \ | awk ' - // { - print ""; + /"; system( "awk \"/body/{i=1;next;} i\" includes/header.html | '"$shref"'" ); next }