--- a/build Tue May 17 01:24:19 2005 +0200
+++ b/build Tue May 17 09:58:40 2005 +0200
@@ -7,7 +7,7 @@
if [ -L "$0" ]; then
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
- exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+ exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
fi
@@ -18,13 +18,12 @@
## settings
-PRG="$(basename "$0")"
-
export THIS_IS_ISABELLE_BUILD=true
-ISABELLE_HOME="$(dirname "$0")"
-. "$ISABELLE_HOME/lib/scripts/getsettings" || \
- { echo "$PRG probably not called from its original place!"; exit 2; }
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
## diagnostics