changeset 4746:8b96f2796afd

Use "sh -c pwd" when we want to avoid having the shell fix up the value of $PWD.
author Richard M. Stallman <rms@gnu.org>
date Sun, 19 Sep 1993 20:04:21 +0000
parents 083140e4419f
children 0019d042d4a6
files configure1.in
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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)`"