3.4 Configure Options

These issues are mainly of concern when building SICStus from a source distribution.

Question: [UNIX]

I've changed the arguments to configure, but nothing happens.

The configure script maintains a cache-file called config.cache. This file has to be removed between configure-runs if you've changed the arguments. Alternatively, you can specify --cache-file=/dev/null, causing configure to avoid creating a cache-file entirely.

Question: [UNIX]

The configure script seems to ignore some of my options.

Make sure that there is no site-wide configuration file (config.site). If configure finds one, it will print a message similar to:

     loading site script /usr/local/etc/config.site
     creating cache ./config.cache
     checking SICStus version... 3.8.5
     [...]

In this case, configure has found a config.site in /usr/local/etc.

The solution is to either remove the file or to set the environment variable CONFIG_SITE to an empty file of your choice. For example, assuming csh:

     % setenv CONFIG_SITE ./config.site
     % echo "# empty config.site" > ./config.site