diff options
Diffstat (limited to 'bin')
| -rw-r--r-- | bin/proofgeneral | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/bin/proofgeneral b/bin/proofgeneral index 56a4bef6..05d26724 100644 --- a/bin/proofgeneral +++ b/bin/proofgeneral @@ -75,7 +75,7 @@ do shift; done 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 + if [ -d "$MYDIR/generic" ]; then PGHOME="$MYDIR" elif [ -d "$PGHOMEDEFAULT" ]; then PGHOME="$PGHOMEDEFAULT" |