Info documentation index
Info documentation index
This is the directory file \`index.html' a.k.a. \`DIR', which contains the
topmost node of the HTML Info hierarchy.
EOF
#list
for i in $document_dirs; do
cat < $i ($i as one big page)
EOF
done >> $index_file
# foot
cat >> $index_file <