diff options
| author | David Aspinall | 2015-02-02 12:59:17 +0000 |
|---|---|---|
| committer | David Aspinall | 2015-02-02 12:59:17 +0000 |
| commit | 806cd783045d19c985eec4863b9a488535ae331a (patch) | |
| tree | 3f857ee6014b81a5eda461a840df4e4452ae875f /bin | |
| parent | 63a2d1e0b425f6bb60dcb21dc2dcb91d4c01cc72 (diff) | |
Fix test defeated by binary install
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" |