include "Isabelle" link;
authorwenzelm
Mon, 25 Sep 2000 12:04:10 +0200
changeset 10068 46db6fde4ee3
parent 10067 ab03cfd6be3a
child 10069 c7226e6f9625
include "Isabelle" link;
Admin/makedist
Admin/makerpm
--- a/Admin/makedist	Sat Sep 23 16:12:07 2000 +0200
+++ b/Admin/makedist	Mon Sep 25 12:04:10 2000 +0200
@@ -198,6 +198,9 @@
 
 cd "$DISTBASE"
 
+rm -f Isabelle
+ln -s "$DISTNAME" Isabelle
+
 chown -R "$LOGNAME" "$DISTNAME"
 chgrp -R isabelle "$DISTNAME"
 chmod -R u+w "$DISTNAME"
--- a/Admin/makerpm	Sat Sep 23 16:12:07 2000 +0200
+++ b/Admin/makerpm	Mon Sep 25 12:04:10 2000 +0200
@@ -235,6 +235,7 @@
 
 cat >>$TMP/SPECS/isabelle.spec <<EOF
 %files
+%$ROOT/Isabelle
 %dir $ISABELLE_HOME
 %dir $ISABELLE_HOME/doc
 %dir $ISABELLE_HOME/heaps