| changeset 28650 | a7ba12e0d3b7 |
| parent 28504 | 7ad7d7d6df47 |
| child 29143 | 72c960b2b83e |
| 28649:58ab885469f5 | 28650:a7ba12e0d3b7 |
|---|---|
15 PRG="$(basename "$0")" |
15 PRG="$(basename "$0")" |
16 |
16 |
17 function usage() |
17 function usage() |
18 { |
18 { |
19 echo |
19 echo |
20 echo "Usage: $PRG [ARGS ...]" |
20 echo "Usage: isabelle $PRG [ARGS ...]" |
21 echo |
21 echo |
22 echo " Apply isabelle make to all logics (passing ARGS)." |
22 echo " Apply isabelle make to all logics (passing ARGS)." |
23 echo |
23 echo |
24 exit 1 |
24 exit 1 |
25 } |
25 } |