| author | wenzelm |
| Mon, 01 Oct 2007 21:19:52 +0200 | |
| changeset 24804 | 513bb015b469 |
| parent 24206 | 9572c9374dc6 |
| child 28500 | 4b79e5d3d0aa |
| 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 |
|
| 24206 | 25 |
"$ISATOOL" mkdir -b -q "$NAME" |
26 |
(cd document; "$ISATOOL" latex -o sty) |
|
|
24185
cb0c4bd149a6
Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff
changeset
|
27 |