equal
deleted
inserted
replaced
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: $PRG [OPTIONS]" |
14 echo "Usage: isabelle $PRG [OPTIONS]" |
15 echo |
15 echo |
16 echo " Options are:" |
16 echo " Options are:" |
17 echo " -d DISTDIR refer to DISTDIR as Isabelle distribution" |
17 echo " -d DISTDIR refer to DISTDIR as Isabelle distribution" |
18 echo " (default ISABELLE_HOME)" |
18 echo " (default ISABELLE_HOME)" |
19 echo " -p DIR install standalone binaries in DIR" |
19 echo " -p DIR install standalone binaries in DIR" |