chiark / gitweb /
Most of intro section
[disorder] / scripts / htmlman
index fa966dda477eddc870a0005e26a6261101ddc15b..21452dce500c0df6a45e6cba9ff887befc6ecd34 100755 (executable)
@@ -3,20 +3,18 @@
 # This file is part of DisOrder
 # Copyright (C) 2004, 2005, 2007, 2008 Richard Kettlewell
 #
-# This program is free software; you can redistribute it and/or modify
+# This program is free software: you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
-# the Free Software Foundation; either version 2 of the License, or
+# the Free Software Foundation, either version 3 of the License, or
 # (at your option) any later version.
-#
-# This program is distributed in the hope that it will be useful, but
-# WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-# General Public License for more details.
-#
+# 
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+# 
 # You should have received a copy of the GNU General Public License
-# along with this program; if not, write to the Free Software
-# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
-# USA
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
 #
 
 set -e
@@ -43,13 +41,13 @@ title=$(basename $1)
 echo "<html>"
 echo " <head>"
 if $stdhead; then
-  echo "@include{stdhead}@"
+  echo "@quiethead@#"
 fi
 echo "  <title>$title</title>"
 echo " </head>"
 echo " <body>"
 if $stdhead; then
-  echo "@include{topbar}@"
+  echo "@stdmenu{}@#"
 fi
 printf "   <pre class=manpage>"
 # this is kind of painful using only BREs
@@ -67,7 +65,7 @@ nroff -Tascii -man "$1" | ${GNUSED} \
                        s!</\([bi]\)><\1>!!g'
 echo "</pre>"
 if $stdhead; then
-  echo "@include{topbarend}@"
+  echo "@credits"
 fi
 echo " </body>"
 echo "</html>"