94828070ed
And fixes the default value of $PGHOME
16 lines
640 B
Diff
16 lines
640 B
Diff
diff -r c7d8bfff4c0a bin/proofgeneral
|
|
--- a/bin/proofgeneral Sat Sep 27 02:25:15 2014 +0100
|
|
+++ b/bin/proofgeneral Sat Sep 27 02:28:16 2014 +0100
|
|
@@ -73,11 +73,7 @@
|
|
|
|
# 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" ]; then
|
|
- PGHOME="$MYDIR"
|
|
- elif [ -d "$PGHOMEDEFAULT" ]; then
|
|
+ if [ -d "$PGHOMEDEFAULT" ]; then
|
|
PGHOME="$PGHOMEDEFAULT"
|
|
else
|
|
echo "Cannot find the Proof General lisp files: Set PGHOME or use --pghome."
|