author | wenzelm |
Tue, 26 Apr 2005 19:51:28 +0200 | |
changeset 15849 | a2c8160b58fd |
parent 15848 | 3001067227af |
child 15850 | 30e878979457 |
--- a/lib/scripts/getsettings Tue Apr 26 19:51:12 2005 +0200 +++ b/lib/scripts/getsettings Tue Apr 26 19:51:28 2005 +0200 @@ -13,7 +13,7 @@ ISABELLE_SETTINGS_PRESENT=true #normalize ISABELLE_HOME as passed by caller -ISABELLE_HOME=$(cd "$ISABELLE_HOME"; echo "$PWD") +ISABELLE_HOME=$(cd "$ISABELLE_HOME"; pwd) if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; } then echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"