tuned;
authorwenzelm
Tue, 26 Apr 2005 19:51:28 +0200
changeset 15849 a2c8160b58fd
parent 15848 3001067227af
child 15850 30e878979457
tuned;
lib/scripts/getsettings
--- 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!"