summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2017-06-08 09:31:14 +0100
committerJeremie Dimino <jeremie@dimino.org>2018-02-12 08:29:16 +0000
commit4d79045d9597f2ba6e48d8cd11b4d3d6a9b6958a (patch)
treece15e9e2e3cc6ca526e20ca7ad43ad7cc2b09a93 /configure
parent225d1c65b9f284b2cd85b26b58698da342ce9792 (diff)
downloadocaml-4d79045d9597f2ba6e48d8cd11b4d3d6a9b6958a.tar.gz
Use gawk on Windows in the build system
awk is symbolic link in Cygwin, which means it can't be used in -pp for a native Windows build. Just use gawk instead, as no other package provides the awk command on Cygwin.
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure1
1 files changed, 1 insertions, 0 deletions
diff --git a/configure b/configure
index 10a171eb3e..be7c8b7ae9 100755
--- a/configure
+++ b/configure
@@ -2136,6 +2136,7 @@ config WINDOWS_UNICODE "0"
config AFL_INSTRUMENT "$afl_instrument"
config MAX_TESTSUITE_DIR_RETRIES "$max_testsuite_dir_retries"
config FLAT_FLOAT_ARRAY "$flat_float_array"
+config AWK "awk"
rm -f tst hasgot.c