| author | wenzelm |
| Wed, 13 Feb 2013 12:06:21 +0100 | |
| changeset 52226 | ced7163f1fe4 |
| parent 29143 | 72c960b2b83e |
| permissions | -rwxr-xr-x |
1 #!/usr/bin/env bash
2 #
3 # Author: David Aspinall
4 #
5 # DESCRIPTION: prepare a session directory for PG-Eclipse
7 PRG="$(basename "$0")"
9 function usage()
10 {
11 echo
12 echo "Usage: isabelle $PRG NAME"
13 echo
14 echo " Prepare a session directory for PG-Eclipse."
15 exit 1
16 }
18 if [ "$#" -eq 1 ]; then
19 NAME="$1"; shift
20 else
21 usage
22 fi
24 "$ISABELLE_TOOL" mkdir -b -q "$NAME"
25 ( cd document; "$ISABELLE_TOOL" latex -o sty; )