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.
This is all very much Work in Progress (WiP).
EOF
#list
for i in $document_dirs; do
echo "- $i
"
done >> $index_file
# foot
cat >> $index_file <