Compile Ciao in an arbitrary subdirectory

Author(s): Manuel Carro.

A simple bash script for compile the whole Ciao distribution, in order to test automatically whether something is broken.

Usage (auto_compile_ciao)

   Usage: auto_compile_ciao ciaodir_name destdir_name
   

More details (auto_compile_ciao)

The script copies the ciao distribution passed on as first argument to a subdirectory of the directory name passed as second argument. The subdirectory is always the same, in order to speed up tests made repeteadly in a distribution. It also deletes from the destination files which do not appear any longer in the sources, and tries not to copy files which will eventually be generated or deleted prior to compilation.

After that, the SETTINGS file is updated to reflect the new location, the sources are cleaned up, and a regular compilation is started.