diff -r c0f9b956a3e7 -r c49d17fac066 Admin/makerpm
--- a/Admin/makerpm	Mon Sep 06 16:57:53 1999 +0200
+++ b/Admin/makerpm	Mon Sep 06 16:59:46 1999 +0200
@@ -22,7 +22,7 @@
   echo
   echo "Usage: $PRG ARCHIVE"
   echo
-  echo "Make Isabelle rpm packages for Linux/x86 from distribution ARCHIVE."
+  echo "Make Isabelle rpm packages for Linux/x86 from the distribution archives."
   echo
   exit 1
 }
@@ -36,21 +36,25 @@
 
 ## process command line
 
-[ $# -ne 1 ] && usage
+[ $# -gt 1 ] && usage
 
-ARCHIVE="$1"
-shift
+ARCHIVE="$1"; shift
+
 
 
 ## main
 
 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
 ARCHIVE_BASE=$(basename "$ARCHIVE")
-ARCHIVE_FULL=$(cd $(dirname "$ARCHIVE"); echo $PWD)/$ARCHIVE_BASE
+ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo $PWD)
+ARCHIVE_FULL=$ARCHIVE_DIR/$ARCHIVE_BASE
 
 ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
 ISABELLE_HOME="$ROOT/$ISABELLE_NAME"
 
+PDF_ARCHIVE_FULL="$ARCHIVE_DIR/${ISABELLE_NAME}_pdf.tar.gz"
+[ ! -f "$PDF_ARCHIVE_FULL" ] && PDF_ARCHIVE_FULL=""
+
 
 # prep
 
@@ -59,12 +63,13 @@
 
 cd "$TMP/BUILD$ROOT"
 tar -xpzf "$ARCHIVE_FULL"
+[ -n "$PDF_ARCHIVE_FULL" ] && tar -xpzf "$PDF_ARCHIVE_FULL"
 
 
 # build
 
 cd "$TMP/BUILD$ROOT/$ISABELLE_NAME"
-( PATH=/bin:$PATH; BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
+( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
 ./build -bi $LOGICS
 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
 rm -f heaps/${COMPILER}/Pure heaps/${COMPILER}/FOL heaps/${COMPILER}/TLA
@@ -143,7 +148,6 @@
 syntactic and deductive tools available in generic Isabelle.  Isabelle
 proof tools provide a high degree of automation.
 
-
 %package	HOL
 Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
 Group:		Applications/Math
@@ -151,7 +155,6 @@
 %description HOL
 This package contains a binary image of the HOL object-logic for Isabelle.
 
-
 %package	HOL-Real
 Summary:	Isabelle Theorem Proving Environment -- Higher-Order Logic
 Group:		Applications/Math
@@ -160,7 +163,6 @@
 This package contains a binary image of the HOL object-logic for Isabelle,
 including support for real numbers.
 
-
 %package	ZF
 Summary:	Isabelle Theorem Proving Environment -- Zermelo-Fraenkel set theory
 Group:		Applications/Math
@@ -168,6 +170,14 @@
 %description ZF
 This package contains a binary image of the ZF object-logic for Isabelle.
 
+%package	pdfdocs
+Summary:	Isabelle Theorem Proving Environment -- PDF documentation
+Group:		Applications/Math
+Requires:       isabelle
+%description pdfdocs
+This package contains the Isabelle documentation in PDF.  Note that
+the dvi version is already part of the base package.
+
 
 %prep
 
@@ -181,6 +191,7 @@
 %post HOL
 %post HOL-Real
 %post ZF
+%post pdfdocs
 
 %postun
 rm -f $BIN/Isabelle $BIN/isabelle $BIN/isatool
@@ -188,6 +199,7 @@
 %postun HOL
 %postun HOL-Real
 %postun ZF
+%postun pdfdocs
 
 
 %files HOL
@@ -199,14 +211,27 @@
 %files ZF
 $ISABELLE_HOME/heaps/${COMPILER}/ZF
 
+%files pdfdocs
+EOF
+
+for F in $(ls -1 doc/*.pdf); do
+  echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
+done
+
+
+cat >>$TMP/SPECS/isabelle.spec <<EOF
 %files
 %dir $ISABELLE_HOME
+%dir $ISABELLE_HOME/doc
 %dir $ISABELLE_HOME/heaps
 %dir $ISABELLE_HOME/heaps/${COMPILER}
 EOF
 
-for F in $(ls -1 | grep -v heaps | grep -v browser_info)
-do
+for F in $(ls -1 | grep -v heaps | grep -v browser_info | grep -v doc); do
+  echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
+done
+
+for F in $(ls -1 doc/* | grep -v pdf); do
   echo "$ISABELLE_HOME/$F" >>$TMP/SPECS/isabelle.spec
 done
 
@@ -224,6 +249,7 @@
 cp "isabelle-HOL-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-HOL.i386.rpm"
 cp "isabelle-HOL-Real-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-HOL-Real.i386.rpm"
 cp "isabelle-ZF-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-ZF.i386.rpm"
+cp "isabelle-pdfdocs-$RPMVERSION-1.i386.rpm" "$DISTBASE/rpm/isabelle-pdfdocs.rpm"
 
 # clean up
 cd /