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