Admin/website/conf/distinfo.mak
author haftmann
Fri, 21 Oct 2005 09:54:03 +0200
changeset 17945 2146e292f62f
parent 17943 48ec47217fe2
permissions -rw-r--r--
towards an improved website/makedist integration

# this is a default file

DISTNAME=Isabelle2005
DISTIDENT=Isabelle2005
DISTBASE=/home/proj/isabelle/dist/dist-Isabelle2005