lib/Tools/install
changeset 6450 990e6e2dee26
parent 6417 39941b906910
child 6459 1d13a86bfa6c
     1.1 --- a/lib/Tools/install	Fri Apr 16 18:52:03 1999 +0200
     1.2 +++ b/lib/Tools/install	Mon Apr 19 17:53:38 1999 +0200
     1.3 @@ -34,6 +34,8 @@
     1.4  
     1.5  # options
     1.6  
     1.7 +NO_OPTS=true
     1.8 +
     1.9  DISTDIR="$ISABELLE_HOME"
    1.10  KDE=""
    1.11  BINDIR=""
    1.12 @@ -43,12 +45,15 @@
    1.13    case "$OPT" in
    1.14      d)
    1.15        DISTDIR="$OPTARG"
    1.16 +      NO_OPTS=""
    1.17        ;;
    1.18      k)
    1.19        KDE=true
    1.20 +      NO_OPTS=""
    1.21        ;;
    1.22      p)
    1.23        BINDIR="$OPTARG"
    1.24 +      NO_OPTS=""
    1.25        ;;
    1.26      \?)
    1.27        usage
    1.28 @@ -61,7 +66,7 @@
    1.29  
    1.30  # args
    1.31  
    1.32 -[ $# -ne 0 ] && usage
    1.33 +[ $# -ne 0 -o -n "$NO_OPTS" ] && usage
    1.34  
    1.35  
    1.36  ## main