equal
deleted
inserted
replaced
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG [OPTIONS]" |
13 echo "Usage: $PRG [OPTIONS]" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
16 echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" |
16 echo " -l NAME logic image name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")" |
17 echo " -m MODE add print mode for output" |
17 echo " -m MODE add print mode for output" |
18 echo " -p NAME line editor program name" |
18 echo " -p NAME line editor program name" |
19 echo " (default ISABELLE_LINE_EDITOR=$ISABELLE_LINE_EDITOR)" |
19 echo " (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")" |
20 echo |
20 echo |
21 echo " Run Isabelle process with plain tty interaction, and optional line editor." |
21 echo " Run Isabelle process with plain tty interaction, and optional line editor." |
22 echo |
22 echo |
23 exit 1 |
23 exit 1 |
24 } |
24 } |