author | wenzelm |
Tue, 14 Oct 2008 16:01:36 +0200 | |
changeset 28592 | 824f8390aaa2 |
parent 28500 | 4b79e5d3d0aa |
child 28650 | a7ba12e0d3b7 |
permissions | -rwxr-xr-x |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
2 |
# |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
3 |
# $Id$ |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
4 |
# Author: David Aspinall and Makarius Wenzel |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
5 |
# |
24206 | 6 |
# DESCRIPTION: prepare a session directory for PG-Eclipse |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
7 |
|
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
8 |
PRG="$(basename "$0")" |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
9 |
|
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
10 |
function usage() |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
11 |
{ |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
12 |
echo |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
13 |
echo "Usage: $PRG NAME" |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
14 |
echo |
24206 | 15 |
echo " Prepare a session directory for PG-Eclipse." |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
16 |
exit 1 |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
17 |
} |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
18 |
|
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
19 |
if [ "$#" -eq 1 ]; then |
24206 | 20 |
NAME="$1"; shift |
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
21 |
else |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
22 |
usage |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
23 |
fi |
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
24 |
|
28500 | 25 |
"$ISABELLE_TOOL" mkdir -b -q "$NAME" |
26 |
( cd document; "$ISABELLE_TOOL" latex -o sty; ) |