equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # Author: David Aspinall and Makarius Wenzel |
4 # Author: David Aspinall and Makarius Wenzel |
5 # |
5 # |
6 # DESCRIPTION: prepare Isabelle project, including document subdirectory |
6 # DESCRIPTION: prepare a session directory for PG-Eclipse |
7 # A useful abbreviation of a pair of isatool calls. |
|
8 # |
|
9 |
7 |
10 PRG="$(basename "$0")" |
8 PRG="$(basename "$0")" |
11 |
9 |
12 function usage() |
10 function usage() |
13 { |
11 { |
14 echo |
12 echo |
15 echo "Usage: $PRG NAME" |
13 echo "Usage: $PRG NAME" |
16 echo |
14 echo |
17 echo " Prepare a session directory in the current directory, including IsaMakefile," |
15 echo " Prepare a session directory for PG-Eclipse." |
18 echo " document source and LaTeX files." |
|
19 exit 1 |
16 exit 1 |
20 } |
17 } |
21 |
18 |
22 if [ "$#" -eq 1 ]; then |
19 if [ "$#" -eq 1 ]; then |
23 NAME="$1"; shift |
20 NAME="$1"; shift |
24 else |
21 else |
25 usage |
22 usage |
26 fi |
23 fi |
27 |
24 |
|
25 "$ISATOOL" mkdir -b -q "$NAME" |
|
26 (cd document; "$ISATOOL" latex -o sty) |
28 |
27 |
29 $ISATOOL mkdir -b -q $NAME |
|
30 (cd document; $ISATOOL latex -o sty) |
|
31 |
|