| changeset 75308 | 6ed34e2e04dd |
| parent 74039 | 8c213672f6f3 |
| 75307:dc1c53d14c38 | 75308:6ed34e2e04dd |
|---|---|
9 PRG=$(basename "$0") |
9 PRG=$(basename "$0") |
10 |
10 |
11 function usage() |
11 function usage() |
12 { |
12 { |
13 echo |
13 echo |
14 echo "Usage: isabelle $PRG [OPTIONS] COMPONENT_DIR" |
14 echo "Usage: isabelle $PRG COMPONENT_DIR" |
15 echo |
15 echo |
16 echo " Build component for Isabelle/Java setup tool." |
16 echo " Build component for Isabelle/Java setup tool." |
17 echo |
17 echo |
18 exit 1 |
18 exit 1 |
19 } |
19 } |