summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2017-09-28 13:25:12 +0200
committerMark Shinwell <mshinwell@gmail.com>2017-09-28 12:25:11 +0100
commit46899afd5e16ed51c919909ebf970a8ef9be0ce4 (patch)
tree5e2eb351f190949df2e01f0e5218b2b8891bd76a /configure
parent24aa2d3cb582d03b5b88e9e0c3c84f985e3937e3 (diff)
downloadocaml-46899afd5e16ed51c919909ebf970a8ef9be0ce4.tar.gz
In Sys.getcwd, don't call getwd if HAS_GETWD is not set (follow-up to #1086) (#1335)
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure5
1 files changed, 0 insertions, 5 deletions
diff --git a/configure b/configure
index 6d4df122da..e854b86217 100755
--- a/configure
+++ b/configure
@@ -1305,11 +1305,6 @@ if sh ./hasgot getcwd; then
echo "#define HAS_GETCWD" >> s.h
fi
-if sh ./hasgot getwd; then
- inf "getwd() found."
- echo "#define HAS_GETWD" >> s.h
-fi
-
if sh ./hasgot getpriority setpriority; then
inf "getpriority() found."
echo "#define HAS_GETPRIORITY" >> s.h