improved usage;
authorwenzelm
Mon, 19 Apr 1999 17:53:38 +0200
changeset 6450 990e6e2dee26
parent 6449 d031cb5ea2fc
child 6451 bc943acc5fda
improved usage;
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