]> matita.cs.unibo.it Git - helm.git/blob - helm/configuration/config.cache.pkg
Check missed: the two metasenv were not compared.
[helm.git] / helm / configuration / config.cache.pkg
1 # This file is a shell script that caches the results of configure
2 # tests run on this system so they can be shared between configure
3 # scripts and configure runs.  It is not useful on other systems.
4 # If it contains results you don't want to keep, you may remove or edit it.
5 #
6 # By default, configure uses ./config.cache as the cache file,
7 # creating it if it does not exist already.  You can give configure
8 # the --cache-file=FILE option to use a different cache file; that is
9 # what configure does when it calls configure scripts in
10 # subdirectories, so they share the cache.
11 # Giving --cache-file=/dev/null disables caching, for debugging configure.
12 # config.status only pays attention to the cache file if you give it the
13 # --recheck option to rerun configure.
14 #
15 helm_cv_HELM_VAR_DIR=${helm_cv_HELM_VAR_DIR='/var/local/helm'}