Admin/website/conf/distinfo.mak
changeset 17945 2146e292f62f
parent 17943 48ec47217fe2
equal deleted inserted replaced
17944:f5ff234ce6b3 17945:2146e292f62f
     1 # this is a generated file - do not edit!
     1 # this is a default file
     2 
     2 
     3 DISTNAME=Isabelle2005
     3 DISTNAME=Isabelle2005
     4 DISTIDENT=Isabelle2005
     4 DISTIDENT=Isabelle2005
     5 DISTBASE=/home/proj/isabelle/dist/dist-Isabelle2005
     5 DISTBASE=/home/proj/isabelle/dist/dist-Isabelle2005