diff -r 7c517c92d315 -r f196352201d6 lib/Tools/mkproject
--- a/lib/Tools/mkproject	Sat May 11 18:16:17 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: David Aspinall
-#
-# DESCRIPTION: prepare a session directory for PG-Eclipse
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG NAME"
-  echo
-  echo "  Prepare a session directory for PG-Eclipse."
-  exit 1
-}
-
-if [ "$#" -eq 1 ]; then
-  NAME="$1"; shift
-else
-  usage
-fi
-
-"$ISABELLE_TOOL" mkdir -b -q "$NAME"
-( cd document; "$ISABELLE_TOOL" latex -o sty; )