# HG changeset patch
# User Richard M. Stallman <rms@gnu.org>
# Date 748469061 0
# Node ID 8b96f2796afd0287063f47e47fedd8473944485f
# Parent  083140e4419f276b624185612dc031d4a4fe0c0b
Use "sh -c pwd" when we want to avoid having the
shell fix up the value of $PWD.

diff -r 083140e4419f -r 8b96f2796afd configure1.in
--- a/configure1.in	Sun Sep 19 19:54:04 1993 +0000
+++ b/configure1.in	Sun Sep 19 20:04:21 1993 +0000
@@ -353,7 +353,7 @@
   . )
     ## We may be able to use the $PWD environment variable to make this
     ## absolute.  But sometimes PWD is inaccurate.
-    if [ "${PWD}" != "" ] && [ "`(cd ${PWD} ; pwd)`" = "`pwd`" ] ; then
+    if [ "${PWD}" != "" ] && [ "`(cd ${PWD} ; sh -c pwd)`" = "`pwd`" ] ; then
       srcdir="$PWD"
     else
       srcdir="`(cd ${srcdir}; pwd)`"