| author | immler@in.tum.de |
| Fri, 09 Nov 2012 14:31:26 +0100 | |
| changeset 50042 | 6fe18351e9dd |
| parent 29143 | 72c960b2b83e |
| permissions | -rwxr-xr-x |
#!/usr/bin/env bash # # Author: David Aspinall # # DESCRIPTION: prepare a session directory for PG-Eclipse PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG NAME" echo echo " Prepare a session directory for PG-Eclipse." exit 1 } if [ "$#" -eq 1 ]; then NAME="$1"; shift else usage fi "$ISABELLE_TOOL" mkdir -b -q "$NAME" ( cd document; "$ISABELLE_TOOL" latex -o sty; )