lib/Tools/mkproject
author wenzelm
Sat, 04 Oct 2008 16:05:09 +0200
changeset 28500 4b79e5d3d0aa
parent 24206 9572c9374dc6
child 28650 a7ba12e0d3b7
permissions -rwxr-xr-x
replaced ISATOOL by ISABELLE_TOOL;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
9572c9374dc6 fixed DESCRIPTION: single line;
wenzelm
parents: 24185
diff changeset
     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
9572c9374dc6 fixed DESCRIPTION: single line;
wenzelm
parents: 24185
diff changeset
    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
9572c9374dc6 fixed DESCRIPTION: single line;
wenzelm
parents: 24185
diff changeset
    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
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 24206
diff changeset
    25
"$ISABELLE_TOOL" mkdir -b -q "$NAME"
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 24206
diff changeset
    26
( cd document; "$ISABELLE_TOOL" latex -o sty; )