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