# HG changeset patch # User wenzelm # Date 1186679963 -7200 # Node ID 9572c9374dc6aa99ad980783491ec0aaf52cae51 # Parent c315d0a40db66e69573697911470d9bf494de377 fixed DESCRIPTION: single line; proper quoting of shell variables; diff -r c315d0a40db6 -r 9572c9374dc6 lib/Tools/mkproject --- a/lib/Tools/mkproject Thu Aug 09 19:00:31 2007 +0200 +++ b/lib/Tools/mkproject Thu Aug 09 19:19:23 2007 +0200 @@ -3,9 +3,7 @@ # $Id$ # Author: David Aspinall and Makarius Wenzel # -# DESCRIPTION: prepare Isabelle project, including document subdirectory -# A useful abbreviation of a pair of isatool calls. -# +# DESCRIPTION: prepare a session directory for PG-Eclipse PRG="$(basename "$0")" @@ -14,18 +12,16 @@ echo echo "Usage: $PRG NAME" echo - echo " Prepare a session directory in the current directory, including IsaMakefile," - echo " document source and LaTeX files." + echo " Prepare a session directory for PG-Eclipse." exit 1 } if [ "$#" -eq 1 ]; then - NAME="$1"; shift + NAME="$1"; shift else usage fi +"$ISATOOL" mkdir -b -q "$NAME" +(cd document; "$ISATOOL" latex -o sty) -$ISATOOL mkdir -b -q $NAME -(cd document; $ISATOOL latex -o sty) -