tuned rpm file names;
authorwenzelm
Wed, 05 May 1999 14:31:31 +0200
changeset 6591 6a753a6d6738
parent 6590 fa5f2ca893c5
child 6592 c120262044b6
tuned rpm file names;
Admin/makerpm
--- a/Admin/makerpm	Wed May 05 14:31:17 1999 +0200
+++ b/Admin/makerpm	Wed May 05 14:31:31 1999 +0200
@@ -191,8 +191,8 @@
 mkdir -p "$DISTBASE/rpm"
 cd "$TMP/RPMS/i386"
 cp "isabelle-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle.rpm"
-cp "isabelle-HOL-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-HOL.i386.rpm"
-cp "isabelle-ZF-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-ZF.i386.rpm"
+cp "isabelle-HOL-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isa-HOL.rpm"
+cp "isabelle-ZF-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isa-ZF.rpm"
 
 # clean up
 cd /