diff options
author | schmidt <douglascraigschmidt@users.noreply.github.com> | 1999-08-09 21:09:45 +0000 |
---|---|---|
committer | schmidt <douglascraigschmidt@users.noreply.github.com> | 1999-08-09 21:09:45 +0000 |
commit | cd1df2b13e2513d28bce827e4530b02cf98d78bf (patch) | |
tree | e6b894bf2ea69ea67fc7d5c430500b8a21e2d1e5 /bin/html-windex | |
parent | 10111d6c554b433095e4f66bb01d1f804165a497 (diff) | |
download | ATCD-cd1df2b13e2513d28bce827e4530b02cf98d78bf.tar.gz |
ChangeLogTag:Mon Aug 9 11:29:36 1999 Douglas C. Schmidt <schmidt@tango.cs.wustl.edu>
Diffstat (limited to 'bin/html-windex')
-rwxr-xr-x | bin/html-windex | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/bin/html-windex b/bin/html-windex index 8047593ade5..153023a1621 100755 --- a/bin/html-windex +++ b/bin/html-windex @@ -1,16 +1,17 @@ -#! /bin/sh -# $Id$ +#!/bin/sh # # This script generates automatically to its stdout a windex.html file; # this file is useful just after running man2html. # All the html man pages must be located under an html directory at the # same level as the generated windex.html file. +# + WINDEX=$1 cat <<EOF - <!-- This is an automatically generated file. Do Not Edit! - Use html-windex to generate it --> + <!-- This is an automatically generated file. Do Not Edit! + Use windex2html to generate it --> <center><h1>ACE Manual Page Index</h1></center> <BODY text = "#000000" link="#000fff" @@ -33,11 +34,11 @@ EOF cat $WINDEX | \ sed -e 's/ / /g' \ - -e 's%\(3\).*-%3\)</a>%g' \ - -e 's/^[a-zA-Z_]*/&\.html">/g' \ + -e 's/^[a-zA-Z0-9_]*/&\.html">/g' \ + -e 's%(3).*-%(3)</a>%g' \ -e 's/\.PP/<BR>/g' \ -e 's%^%<li><a HREF="html/%g' \ - -e 's%\\f(CO[a-zA-Z_]*%<CODE>&</B></I></CODE>%g' \ + -e 's%\\f(CO[a-zA-Z0-9_]*%<CODE>&</B></I></CODE>%g' \ -e 's%\\f(CO%%g' echo "</UL>" |