#! /bin/csh -f
# Last edited on 1999-01-29 20:21:56 by stolfi

set usage = "$0 DIR FNUM TITLE"

# If DIR/FNUM exists, appends it to html/FNUM.html, properly
# formatted as a section, with the given section TITLE.

if ( $#argv != 3 ) then
  echo "usage: $usage" > /dev/stderr; exit 1
endif

set dir   = "$1"; shift;
set fnum  = "$1"; shift;
set title = "$1"; shift;

if ( ! -w html/${fnum}.html ) then
  echo "$0: html/${fnum}.html not writable - aborted" > /dev/stderr;
  exit 1
endif

if ( -r ${dir}/${fnum} ) then
  cat ${dir}/${fnum} \
    | format-html-section \
        -v title="${title}" \
        -v exdent=2 \
    >> html/${fnum}.html
else
  echo "warning: ${dir}/${fnum} not found" > /dev/stderr
endif