diff options
| author | David Allsopp <david.allsopp@metastack.com> | 2022-09-28 19:17:10 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-09-28 20:17:10 +0200 |
| commit | 99a126992df5da2c2431bf75a4b11e51bd1724b9 (patch) | |
| tree | d7de90ad1c3a4076106f52b190acc709e27654a9 /tools | |
| parent | 3ac4643e7863ecadbd4f3eaa17a162bafa733a3c (diff) | |
| download | ocaml-99a126992df5da2c2431bf75a4b11e51bd1724b9.tar.gz | |
Switch required autoconf to 2.71 (#11294)
* Switch required autoconf to 2.71
Minimum version moves with the GitHub Actions runners supported version
on Ubuntu.
* Remove unneeded patching from configure
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/autogen | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/tools/autogen b/tools/autogen index 69cc910180..cd9f6d2fbc 100755 --- a/tools/autogen +++ b/tools/autogen @@ -22,18 +22,9 @@ ${1-autoconf} --force --warnings=all,error # The sed call removes dra27's copyright on the whole configure script... sed -e '/^#[^!]/d' tools/git-dev-options.sh > configure.tmp -# Some distros have the 2013 --runstatedir patch to autoconf (see -# http://git.savannah.gnu.org/cgit/autoconf.git/commit/?id=a197431414088a417b407b9b20583b2e8f7363bd -# in the GNU autoconf repo), and some don't, so ensure its effects are -# removed for CI consistency... -# POSIX Notes -# - sed -i without a backup file is not portable, hence configure.tmp -# - GNU sed's /../,+8d becomes /../{N;..;d;} (and the last ; is important) -sed -e '/^runstatedir/d' \ - -e '/-runstatedir /{N;N;N;N;N;N;N;N;d;}' \ - -e '/--runstatedir=DIR/d' \ - -e 's/ runstatedir//' \ - -e '/split(line, arg/s|" "|/[ \\r\\t]/|' \ +# - Workaround sr #110554 (https://savannah.gnu.org/support/index.php?110554) +# - sed -i without a backup file is not portable, hence configure.tmp +sed -e '/split(line, arg/s|" "|/[ \\r\\t]/|' \ -e '/define|undef/s/|\\\$/|\\r?\\$/' \ -e '1d' \ configure >> configure.tmp |