diff options
Diffstat (limited to 'bin')
| -rw-r--r-- | bin/proofgeneral | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/bin/proofgeneral b/bin/proofgeneral index a661adaf..00c5d620 100644 --- a/bin/proofgeneral +++ b/bin/proofgeneral @@ -74,8 +74,9 @@ do shift; done # Try to find Proof General directory if [ -z "$PGHOME" ] || [ ! -d "$PGHOME" ]; then # default relative to this script, otherwise PGHOMEDEFAULT - if [ -d ../generic ]; then - PGHOME="../generic" + MYDIR="`readlink --canonicalize "$0" | sed -ne 's,/bin/proofgeneral$,,p'`" + if [ -d "$MYDIR" ]; then + PGHOME="$MYDIR" elif [ -d "$PGHOMEDEFAULT" ]; then PGHOME="$PGHOMEDEFAULT" else |