#! /bin/sh

# This script should be run by executing
#   make DOC
# or
#   make HTML
# from the main ACL2 directory.  The make variable PREFIX is used in this script.

rm -f doc/workxxx

# The next two non-blank lines should be commented out if we don't want to
# destroy what's in the saved/ subdirectory.

rm -f doc/HTML/saved/*
touch doc/HTML/temp.temp
mv -f doc/HTML/*.* doc/HTML/saved

cd doc/HTML

# Some ACL2 images start up inside LP; some don't.  (value :q) always gets us
# out of the loop, and should also be harmless when executed in raw Lisp.
# However, note that Lispworks requires that the two forms not all be on the
# same line.

echo '(value :q)' > workxxx
echo '(lp)' >> workxxx

echo '(certify-book (:RELATIVE :BACK "write-acl2-html"))' >> workxxx

echo '(write-html-file :file "acl2-doc")' >> workxxx

echo ':q' >> workxxx

../../${PREFIX}saved_acl2 < workxxx

# To debug bad documentation:
# Start up ACL2 in the source directory.
# (include-book "doc/write-acl2-texinfo")
# Apply DEFDOC to fix bad documentation.
# (write-html-file :file "acl2-doc")