src/Tools/Cache_IO/etc/settings
changeset 35140 117247018b54
equal deleted inserted replaced
35139:082fa4bd403d 35140:117247018b54
       
     1 ISABELLE_CACHE_IO="$COMPONENT"
       
     2 
       
     3 COMPUTE_HASH_KEY="$ISABELLE_CACHE_IO/lib/scripts/compute_hash_key"
       
     4