# gendocs.sh -- generate a GNU manual in many formats. This script is
# mentioned in maintain.texi. See the help message below for usage details.
# gendocs.sh -- generate a GNU manual in many formats. This script is
# mentioned in maintain.texi. See the help message below for usage details.
dirargs= # passed to all tools (-I dir).
dirs= # -I directories.
htmlarg="--css-ref=/software/gnulib/manual.css -c TOP_NODE_UP_URL=/manual"
dirargs= # passed to all tools (-I dir).
dirs= # -I directories.
htmlarg="--css-ref=/software/gnulib/manual.css -c TOP_NODE_UP_URL=/manual"
--info) shift; infoarg=$1;;
--no-ascii) generate_ascii=false;;
--no-html) generate_ascii=false;;
--info) shift; infoarg=$1;;
--no-ascii) generate_ascii=false;;
--no-html) generate_ascii=false;;
if test -n "$srcfile"; then
# but here, we use the basename of $srcfile
base=`basename "$srcfile"`
if test -n "$srcfile"; then
# but here, we use the basename of $srcfile
base=`basename "$srcfile"`