# HG changeset patch
# User aspinall
# Date 1113498967 -7200
# Node ID 75b9219980d3018c5860a1a779d30f09ea813d3f
# Parent  faa48c5b14021b83e45fc24d4aa169dade2e344f
Add RDISTDIR option used by Isabelle RPM.

diff -r faa48c5b1402 -r 75b9219980d3 lib/Tools/install
--- a/lib/Tools/install	Thu Apr 14 17:57:23 2005 +0200
+++ b/lib/Tools/install	Thu Apr 14 19:16:07 2005 +0200
@@ -16,6 +16,9 @@
   echo "  Options are:"
   echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"
   echo "                 (default ISABELLE_HOME)"
+  echo "    -a RDISTDIR  refer to RDISTDIR as Isabelle distribution"
+  echo "                 in installed files, for packaging scripts"
+  echo "                 (default to same value as -d)"
   echo "    -k VERSION   install KDE application icon on desktop"
   echo "                 (for KDE VERSION 1 or 2)"
   echo "    -p DIR       install standalone binaries in DIR"
@@ -42,8 +45,9 @@
 DISTDIR="$ISABELLE_HOME"
 KDE=""
 BINDIR=""
+RDISTDIR=""
 
-while getopts "d:k:p:" OPT
+while getopts "d:k:p:a:" OPT
 do
   case "$OPT" in
     d)
@@ -58,6 +62,10 @@
       BINDIR="$OPTARG"
       NO_OPTS=""
       ;;
+    a)
+      RDISTDIR="$OPTARG"
+      NO_OPTS=""
+      ;;
     \?)
       usage
       ;;
@@ -71,6 +79,9 @@
 
 [ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
 
+if [ -z "$RDISTDIR" ]; then
+  RDISTDIR=$DISTDIR
+fi
 
 ## main
 
@@ -97,7 +108,7 @@
   for NAME in isatool isabelle-process isabelle-interface
   do
     BIN="$BINDIR/$NAME"
-    DIST="$DISTDIR/bin/$NAME"
+    DIST="$RDISTDIR/bin/$NAME"
     echo "installing $BIN"
     echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN"
     echo >> "$BIN"
@@ -145,7 +156,7 @@
   echo "# KDE Config File" > "$KDEAPP" || fail "Cannot write file: $KDEAPP"
   echo "[KDE Desktop Entry]" >> "$KDEAPP"
   echo "Type=Application" >> "$KDEAPP"
-  echo "Exec=\"$DISTDIR/bin/isabelle-interface\" %f" >> "$KDEAPP"
+  echo "Exec=\"$RDISTDIR/bin/isabelle-interface\" %f" >> "$KDEAPP"
   echo "Icon=isabelle.xpm" >> "$KDEAPP"
   echo "TerminalOptions=" >> "$KDEAPP"
   echo "Path=" >> "$KDEAPP"