fixed DESCRIPTION: single line;
authorwenzelm
Thu Aug 09 19:19:23 2007 +0200 (2007-08-09)
changeset 242069572c9374dc6
parent 24205 c315d0a40db6
child 24207 402d629925ed
fixed DESCRIPTION: single line;
proper quoting of shell variables;
lib/Tools/mkproject
     1.1 --- a/lib/Tools/mkproject	Thu Aug 09 19:00:31 2007 +0200
     1.2 +++ b/lib/Tools/mkproject	Thu Aug 09 19:19:23 2007 +0200
     1.3 @@ -3,9 +3,7 @@
     1.4  # $Id$
     1.5  # Author: David Aspinall and Makarius Wenzel
     1.6  #
     1.7 -# DESCRIPTION: prepare Isabelle project, including document subdirectory
     1.8 -# A useful abbreviation of a pair of isatool calls.
     1.9 -#
    1.10 +# DESCRIPTION: prepare a session directory for PG-Eclipse
    1.11  
    1.12  PRG="$(basename "$0")"
    1.13  
    1.14 @@ -14,18 +12,16 @@
    1.15    echo
    1.16    echo "Usage: $PRG NAME"
    1.17    echo
    1.18 -  echo "  Prepare a session directory in the current directory, including IsaMakefile,"
    1.19 -  echo "  document source and LaTeX files."
    1.20 +  echo "  Prepare a session directory for PG-Eclipse."
    1.21    exit 1
    1.22  }
    1.23  
    1.24  if [ "$#" -eq 1 ]; then
    1.25 -   NAME="$1"; shift
    1.26 +  NAME="$1"; shift
    1.27  else
    1.28    usage
    1.29  fi
    1.30  
    1.31 +"$ISATOOL" mkdir -b -q "$NAME"
    1.32 +(cd document; "$ISATOOL" latex -o sty)
    1.33  
    1.34 -$ISATOOL mkdir -b -q $NAME
    1.35 -(cd document; $ISATOOL latex -o sty)
    1.36 -