# A sub script to doc2html.  Not to be run independently.
cnt=0
read line
while [ TRUE ]; do
if [ "`echo $line | grep "%"`" ]; then
  if [ "$cnt" -eq 1 ]; then
   echo "<PRE>"
   echo;echo;echo;echo;echo;echo;echo;echo;echo;echo
   echo "</PRE><HR>"
  fi
  cnt=1
  line1=$line
  line=`echo "<A NAME=\"$line1\"><P><B>Code [$line1]</B><P>"|sed -e "s/%//g"`
fi
if [ -z "$line" ]; then
  echo "<P>"
else
  echo $line
fi
read line
if [ `echo $?` -ne 0 ]; then exit; fi
done
