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