Remove bin/proofgeneral and Update Makefiles accordingly.

Closes ProofGeneral/PG#177

3 files changed, 6 insertions, 123 deletions

diff --git a/Makefile b/Makefile
index 78e4394f..c629a4bc 100644
--- a/Makefile
+++ b/Makefile
@@ -46,16 +46,11 @@ DOC_SUBDIRS=${DOC_EXAMPLES} */README* */CHANGES */BUGS
 BATCHEMACS=${EMACS} --batch --no-site-file -q 
 
 # Scripts to edit paths to shells
-BASH_SCRIPTS = isar/interface bin/proofgeneral
+BASH_SCRIPTS = isar/interface
 PERL_SCRIPTS = lego/legotags coq/coqtags isar/isartags
-# Scripts to edit path to PG
-# the scripts target (part of install) and the cleanscripts target
-# (part of clean) work only under the assumption that PG_SCRIPTS is a subset of
-# the union of BASH_SCRIPTS and PERL_SCRIPTS.
-PG_SCRIPTS = bin/proofgeneral
 
 # Scripts to install to bin directory
-BIN_SCRIPTS = bin/proofgeneral lego/legotags coq/coqtags isar/isartags
+BIN_SCRIPTS = lego/legotags coq/coqtags isar/isartags
 
 # Setting load path might be better in Elisp, but seems tricky to do
 # only during compilation.  Another idea: put a function in proof-site
@@ -236,7 +231,7 @@ doc.%: FORCE
 ## scripts: try to patch bash and perl scripts with correct paths
 ##
 .PHONY: scripts
-scripts: bashscripts perlscripts pgscripts
+scripts: bashscripts perlscripts
 
 .PHONY: bashscripts
 bashscripts:
@@ -260,18 +255,10 @@ perlscripts:
 	   sed -i.orig "s|^#.*!.*/bin/perl.*$$|#!$$perl|" $$i; \
 	 done)
 
-# FIXME: this next edit is really for install case, shouldn't be made
-# just when user types 'make'
-.PHONY: pgscripts
-pgscripts: bashscripts perlscripts
-	(for i in $(PG_SCRIPTS); do \
-	   sed -i.rm "s|PGHOMEDEFAULT=.*$$|PGHOMEDEFAULT=${DEST_ELISP}|" $$i; \
-	 done)
-
 # Set PGHOME path in scripts back to default location.
 .PHONY: cleanscripts
 cleanscripts:
-	(for i in $(PG_SCRIPTS) $(BASH_SCRIPTS) $(PERL_SCRIPTS); do \
+	(for i in $(BASH_SCRIPTS) $(PERL_SCRIPTS); do \
 	   if [ -f $$i.rm ] ; then \
 	     rm -f $$i.rm; \
 	   fi; \
diff --git a/Makefile.devel b/Makefile.devel
index bba2efef..b3b9d58d 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -443,6 +443,8 @@ rpmrelease: rpm
 ##     This requires sudo powers for mounting, and
 ##     (on Ubuntu), packages hfsplus and hfsprogs
 ##
+## Warning: the following line was removed below so Contents/MacOS'll be empty:
+##     mv $(NAME)/bin/proofgeneral Contents/MacOS;
 DMGBUILD=$(DISTBUILDIR)/dmg
 dmg:
 	rm -rf $(DMGBUILD)
@@ -455,7 +457,6 @@ dmg:
 	$(TAR) -xpzf $(DISTBUILDIR)/$(RELEASENAMETGZ); \
 	mkdir -p Contents/Resources; \
 	mkdir -p Contents/MacOS; \
-	mv $(NAME)/bin/proofgeneral Contents/MacOS; \
 	mv $(NAME)/* Contents/Resources; \
 	rm -rf $(NAME) $(RELEASENAME); \
 	mkdir $(NAME).app; \
diff --git a/bin/proofgeneral b/bin/proofgeneral
deleted file mode 100755
index 05d26724..00000000
--- a/bin/proofgeneral
+++ /dev/null
@@ -1,105 +0,0 @@
-#!/bin/sh
-#
-# Simple shell script for launching Proof General.
-#
-# Set EMACS to override choice of Emacs version
-#
-# PGHOME must be set to the directory where the lisp files of Proof
-# General are installed.  Script checks standard locations in
-# /usr/share/emacs/site-lisp, or uses PGHOMEDEFAULT defined at top.
-#
-# We load ~/.proofgeneral instead of ~/.emacs if it exists.
-#
-# Thanks to Achim Brucker for suggestions.
-#
-# $Id$
-#
-
-# The default path should work if you are using the Proof General RPM
-# or unpack Proof General in your home directory.  Otherwise edit below.
-# NB: no trailing backslash here!
-# On Mac, maybe:
-# /Applications/Emacs.app/Contents/MacOS/Emacs/site-lisp/ProofGeneral
-PGHOMEDEFAULT=$HOME/ProofGeneral
-
-NAME=`basename $0`
-
-HELP="Usage: proofgeneral [OPTION] [FILE]...
-Launches Emacs Proof General, editing the proof script FILE.
-
-Options:
-  --emacs <EMACS>     startup Proof General with emacs binary <EMACS>
-  --pghome <PGDIR>    startup Proof General from directory PGDIR
-  -h, --help          show this help and exit
-  -v, --version       output version information and exit
-
-Unrecognized options are passed to Emacs, along with file names.
-
-Examples:
-  $NAME Example.thy   Load Proof General editing Isar file Example.thy
-  $NAME example.v     Load Proof General editing Coq file Example.v
-
-For documentation and latest versions, visit http://proofgeneral.inf.ed.ac.uk
-Report bugs at http://proofgeneral.inf.ed.ac.uk/trac"
-
-VERSIONBLURB='David Aspinall.
-
-Copyright (C) 1998-2009 LFCS, University of Edinburgh, UK.
-This is free software; see the source for copying conditions.'
-
-   
-while 
-  case $1 in 
-    -h) 
-	echo "$HELP"
-	exit 0;;
-    --help)
-	echo "$HELP"
-	exit 0;;
-    --emacs)
-	EMACS="$2"
-	shift;;
-    --pghome)
-	PGHOME="$2"
-	shift;;
-    --version|-v) 
-	VERSION=`grep proof-general-version $PGHOME/generic/proof-site.el | head -1 | sed -e 's/.*Version //g' | sed -e 's/\. .*//g'`
-	echo "$NAME" "--- script to launch Proof General $VERSION"
-	echo "$VERSIONBLURB"
-	exit 0;;
-    *) break;;
-  esac
-do shift; done
-
-# Try to find Proof General directory
-if [ -z "$PGHOME" ] || [ ! -d "$PGHOME" ]; then
-    # default relative to this script, otherwise PGHOMEDEFAULT
-    MYDIR="`readlink --canonicalize "$0" | sed -ne 's,/bin/proofgeneral$,,p'`"
-    if [ -d "$MYDIR/generic" ]; then
-	PGHOME="$MYDIR"
-    elif [ -d "$PGHOMEDEFAULT" ]; then
-	PGHOME="$PGHOMEDEFAULT"
-    else
-	echo "Cannot find the Proof General lisp files: Set PGHOME or use --pghome."
-	exit 1
-    fi
-fi
-
-# Try to find an Emacs executable 
-if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
-    if which emacs > /dev/null; then 
-	EMACS=`which emacs`
-    else 
-	echo "$NAME: cannot find an Emacs executable.  Change PATH, set EMACS, use --emacs to specify." 1>&2
-	exit 1
-    fi 
-fi
-
-# User may use .proofgeneral in preference to .emacs or .xemacs/init.el
-if [ -f $HOME/.proofgeneral ]; then
-    STARTUP="-q -l $HOME/.proofgeneral"
-else
-    STARTUP=""
-fi
-
-exec $EMACS $STARTUP -eval "(or (featurep (quote proof-site)) (load \"$PGHOME/generic/proof-site.el\"))" -f proof-splash-display-screen "$@"