----------------------------------------------------------------------
UPDATE (25 Jul 2008):
Now require users to do their configuration from the root HOL
directory (updating the documentation to reflect this).  The reason is
to enable both
   mosml < tools/smart-configure.sml
and
   poly < tools/smart-configure.sml
The contents of tools/smart-configure.sml now figures out which
interpreter is being run (by relying on a known mosml bug), and then
runs the real configuration script for the given ML system.
----------------------------------------------------------------------


This file explains how to rebuild HOL4 in the directory HOL on my
Linux machine at Cambridge. HOL sould contain:

bin	    doc       install.txt  scheme  std.prelude
COPYRIGHT   examples  Manual	   sigobj  tools
developers  help      README	   src	   tools-poly


To configure and build HOL4 go to the directory HOL and do:

 cd tools;
 mosml < smart-configure.sml ;
 cd ../bin;
 build -symlink 

The "-symlink" is needed so that updates to libraries, specifically
HolBddLib, see below, can easily be made. 

N.B. If a rebuild is being done, then in occasional pathological cases
     you might need to precede the build by "build cleanAll" in HOL/bin

---------------------------------------------------------------------
Mike Gordon
Updated June 2008