src/Tools/Cache_IO/etc/settings
changeset 35140 117247018b54
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/Cache_IO/etc/settings	Tue Feb 16 15:25:36 2010 +0100
     1.3 @@ -0,0 +1,4 @@
     1.4 +ISABELLE_CACHE_IO="$COMPONENT"
     1.5 +
     1.6 +COMPUTE_HASH_KEY="$ISABELLE_CACHE_IO/lib/scripts/compute_hash_key"
     1.7 +