#!/bin/bash
# Make html in html/man from the man pages in the named
# directories
# Config stuff
out_dir=`pwd`/html/man
# print usage and exit
usage() {
echo usage: $0 dir1 dir2 ...
echo make html in $out_dir from the man pages in the
echo named directories
exit 1
}
# If a dir does not exist, make it
makedir() {
if test ! -d "$1"; then
mkdir "$1"
status=$?
if test $status -ne 0 && test ! -d "$1"; then
exit $status
fi
fi
}
makedir `pwd`/html
makedir `pwd`/html/man
makedir $out_dir
# echo the filename given a path
filename() {
echo ${1/#*\//}
}
# echo the dirname given a path... make sure there's a trailing slash
dirname() {
# break off the filename, then junk that many chars off the end of
# $1 to make the dirname
local file=`filename $1`
local dir=${1:0:$((${#1}-${#file}))}
# is dir "/"? return immediately
if test "$dir" == "/"; then
echo "/"
return
fi
# remove trailing slash, provided we're not removing everything
dir=${dir/%\//}
# if there's no dir, we must be in the current dir
if test "$dir" == ""; then
dir="."
fi
# finally add a trailing "/" back again
echo $dir/
}
# Need VIPSHOME
export VIPSHOME=`vips im_guess_prefix im_version VIPSHOME`
: ${VIPSHOME:?}
if test $# -le 0; then
usage
fi
# Loop over args, adding source man pages
for dir in $*; do
if test -d "$dir"; then
files="$files $dir/*.[0-9]"
else
echo "$0: directory $dir does not exist"
exit 1
fi
done
# Make output!
let j=0
for i in $files; do
file=`filename $i`
dir=`dirname $i`
( cd $dir/.. ;
rman -f html -r '%s.%s.html' $dir$file > $out_dir/$file.html )
let j+=1
done
echo "$0: made $j pages of html"