isabelle: lib/Tools/mkproject@c3d1f87a3cb0 (annotated)

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; )

author	huffman
	Wed, 24 Dec 2008 13:39:20 -0800
changeset 29172	c3d1f87a3cb0
parent 29143	72c960b2b83e
permissions	-rwxr-xr-x