equal
deleted
inserted
replaced
32 |
32 |
33 ## process command line |
33 ## process command line |
34 |
34 |
35 # options |
35 # options |
36 |
36 |
|
37 NO_OPTS=true |
|
38 |
37 DISTDIR="$ISABELLE_HOME" |
39 DISTDIR="$ISABELLE_HOME" |
38 KDE="" |
40 KDE="" |
39 BINDIR="" |
41 BINDIR="" |
40 |
42 |
41 while getopts "d:kp:" OPT |
43 while getopts "d:kp:" OPT |
42 do |
44 do |
43 case "$OPT" in |
45 case "$OPT" in |
44 d) |
46 d) |
45 DISTDIR="$OPTARG" |
47 DISTDIR="$OPTARG" |
|
48 NO_OPTS="" |
46 ;; |
49 ;; |
47 k) |
50 k) |
48 KDE=true |
51 KDE=true |
|
52 NO_OPTS="" |
49 ;; |
53 ;; |
50 p) |
54 p) |
51 BINDIR="$OPTARG" |
55 BINDIR="$OPTARG" |
|
56 NO_OPTS="" |
52 ;; |
57 ;; |
53 \?) |
58 \?) |
54 usage |
59 usage |
55 ;; |
60 ;; |
56 esac |
61 esac |
59 shift $(($OPTIND - 1)) |
64 shift $(($OPTIND - 1)) |
60 |
65 |
61 |
66 |
62 # args |
67 # args |
63 |
68 |
64 [ $# -ne 0 ] && usage |
69 [ $# -ne 0 -o -n "$NO_OPTS" ] && usage |
65 |
70 |
66 |
71 |
67 ## main |
72 ## main |
68 |
73 |
69 echo "distribution at $DISTDIR" |
74 echo "distribution at $DISTDIR" |