added default distinfo.mak
authorhaftmann
Fri, 21 Oct 2005 09:08:42 +0200
changeset 17943 48ec47217fe2
parent 17942 68988fd2fd27
child 17944 f5ff234ce6b3
added default distinfo.mak
Admin/website/conf/distinfo.mak
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/conf/distinfo.mak	Fri Oct 21 09:08:42 2005 +0200
@@ -0,0 +1,5 @@
+# this is a generated file - do not edit!
+
+DISTNAME=Isabelle2005
+DISTIDENT=Isabelle2005
+DISTBASE=/home/proj/isabelle/dist/dist-Isabelle2005