# HG changeset patch
# User wenzelm
# Date 924537218 -7200
# Node ID 990e6e2dee2645dce42a29caaeb18f0aee1bcd52
# Parent  d031cb5ea2fcd8503145e111de6e0827dde5ae5a
improved usage;

diff -r d031cb5ea2fc -r 990e6e2dee26 lib/Tools/install
--- a/lib/Tools/install	Fri Apr 16 18:52:03 1999 +0200
+++ b/lib/Tools/install	Mon Apr 19 17:53:38 1999 +0200
@@ -34,6 +34,8 @@
 
 # options
 
+NO_OPTS=true
+
 DISTDIR="$ISABELLE_HOME"
 KDE=""
 BINDIR=""
@@ -43,12 +45,15 @@
   case "$OPT" in
     d)
       DISTDIR="$OPTARG"
+      NO_OPTS=""
       ;;
     k)
       KDE=true
+      NO_OPTS=""
       ;;
     p)
       BINDIR="$OPTARG"
+      NO_OPTS=""
       ;;
     \?)
       usage
@@ -61,7 +66,7 @@
 
 # args
 
-[ $# -ne 0 ] && usage
+[ $# -ne 0 -o -n "$NO_OPTS" ] && usage
 
 
 ## main