| author | wenzelm | 
| Fri, 26 Sep 2008 17:24:15 +0200 | |
| changeset 28374 | 27f1b5cc5f9b | 
| 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  |