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