author | bulwahn |
Tue, 26 Feb 2008 11:18:43 +0100 | |
changeset 26143 | 314c0bcb7df7 |
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 |