| changeset 28650 | a7ba12e0d3b7 |
| parent 28500 | 4b79e5d3d0aa |
| child 29143 | 72c960b2b83e |
| 28649:58ab885469f5 | 28650:a7ba12e0d3b7 |
|---|---|
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 [DOC]" |
14 echo "Usage: isabelle $PRG [DOC]" |
15 echo |
15 echo |
16 echo " View Isabelle documentation DOC, or show list of available documents." |
16 echo " View Isabelle documentation DOC, or show list of available documents." |
17 echo |
17 echo |
18 exit 1 |
18 exit 1 |
19 } |
19 } |