lib/Tools/mkproject
author paulson
Tue, 02 Feb 2010 09:48:20 +0000
changeset 35503 7bba12c3b7b6
parent 29143 72c960b2b83e
permissions -rwxr-xr-x
Correction of a tiny error
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
#
29143
72c960b2b83e removed Ids;
wenzelm
parents: 28650
diff changeset
     3
# Author: David Aspinall
24185
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
     4
#
24206
9572c9374dc6 fixed DESCRIPTION: single line;
wenzelm
parents: 24185
diff changeset
     5
# DESCRIPTION: prepare a session directory for PG-Eclipse
24185
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
     6
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
     7
PRG="$(basename "$0")"
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
     8
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
     9
function usage()
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    10
{
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    11
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 28500
diff changeset
    12
  echo "Usage: isabelle $PRG NAME"
24185
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    13
  echo
24206
9572c9374dc6 fixed DESCRIPTION: single line;
wenzelm
parents: 24185
diff changeset
    14
  echo "  Prepare a session directory for PG-Eclipse."
24185
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    15
  exit 1
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    16
}
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
if [ "$#" -eq 1 ]; then
24206
9572c9374dc6 fixed DESCRIPTION: single line;
wenzelm
parents: 24185
diff changeset
    19
  NAME="$1"; shift
24185
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    20
else
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    21
  usage
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    22
fi
cb0c4bd149a6 Useful abbreviation of isatool commands used by Eclipse
aspinall
parents:
diff changeset
    23
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 24206
diff changeset
    24
"$ISABELLE_TOOL" mkdir -b -q "$NAME"
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 24206
diff changeset
    25
( cd document; "$ISABELLE_TOOL" latex -o sty; )