lib/Tools/mkproject
author wenzelm
Sat Oct 04 16:05:09 2008 +0200 (2008-10-04 ago)
changeset 28500 4b79e5d3d0aa
parent 24206 9572c9374dc6
child 28650 a7ba12e0d3b7
permissions -rwxr-xr-x
replaced ISATOOL by ISABELLE_TOOL;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: David Aspinall and Makarius Wenzel
     5 #
     6 # DESCRIPTION: prepare a session directory for PG-Eclipse
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG NAME"
    14   echo
    15   echo "  Prepare a session directory for PG-Eclipse."
    16   exit 1
    17 }
    18 
    19 if [ "$#" -eq 1 ]; then
    20   NAME="$1"; shift
    21 else
    22   usage
    23 fi
    24 
    25 "$ISABELLE_TOOL" mkdir -b -q "$NAME"
    26 ( cd document; "$ISABELLE_TOOL" latex -o sty; )