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 [ARGS ...]" |
14 echo "Usage: isabelle $PRG [ARGS ...]" |
15 echo |
15 echo |
16 echo " Compile the logic in current directory using IsaMakefile." |
16 echo " Compile the logic in current directory using IsaMakefile." |
17 echo " ARGS are directly passed to the system make program." |
17 echo " ARGS are directly passed to the system make program." |
18 echo |
18 echo |
19 exit 1 |
19 exit 1 |